MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reu4 Unicode version

Theorem reu4 2959
Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 23-Nov-1994.)
Hypothesis
Ref Expression
rmo4.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
reu4  |-  ( E! x  e.  A  ph  <->  ( E. x  e.  A  ph 
/\  A. x  e.  A  A. y  e.  A  ( ( ph  /\  ps )  ->  x  =  y ) ) )
Distinct variable groups:    x, y, A    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem reu4
StepHypRef Expression
1 reu5 2753 . 2  |-  ( E! x  e.  A  ph  <->  ( E. x  e.  A  ph 
/\  E* x  e.  A ph ) )
2 rmo4.1 . . . 4  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
32rmo4 2958 . . 3  |-  ( E* x  e.  A ph  <->  A. x  e.  A  A. y  e.  A  (
( ph  /\  ps )  ->  x  =  y ) )
43anbi2i 675 . 2  |-  ( ( E. x  e.  A  ph 
/\  E* x  e.  A ph )  <->  ( E. x  e.  A  ph  /\  A. x  e.  A  A. y  e.  A  (
( ph  /\  ps )  ->  x  =  y ) ) )
51, 4bitri 240 1  |-  ( E! x  e.  A  ph  <->  ( E. x  e.  A  ph 
/\  A. x  e.  A  A. y  e.  A  ( ( ph  /\  ps )  ->  x  =  y ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wral 2543   E.wrex 2544   E!wreu 2545   E*wrmo 2546
This theorem is referenced by:  reuind  2968  oawordeulem  6552  fin23lem23  7952  nqereu  8553  receu  9413  lbreu  9704  cju  9742  divalglem9  12600  ndvdssub  12606  qredeu  12786  pj1eu  15005  efgredeu  15061  lspsneu  15876  qtopeu  17407  qtophmeo  17508  minveclem7  18799  ig1peu  19557  coeeu  19607  plydivalg  19679  exidu1  20993  rngoideu  21051  minvecolem7  21462  hlimreui  21819  riesz4i  22643  cdjreui  23012  xreceu  23105  cvmseu  23807  nocvxmin  24345  axcontlem2  24593  segconeu  24634  outsideofeu  24754  negveud  25668  negveudr  25669  bfp  26548  mpaaeu  27355  lshpsmreu  29299  cdleme  30749  lcfl7N  31691  mapdpg  31896  hdmap14lem6  32066
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-cleq 2276  df-clel 2279  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551
  Copyright terms: Public domain W3C validator