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

Theorem reu4 3207
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 2985 . 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 3206 . . 3  |-  ( E* x  e.  A  ph  <->  A. x  e.  A  A. y  e.  A  (
( ph  /\  ps )  ->  x  =  y ) )
43anbi2i 698 . 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 252 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 setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370   A.wral 2714   E.wrex 2715   E!wreu 2716   E*wrmo 2717
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-cleq 2421  df-clel 2424  df-ral 2719  df-rex 2720  df-reu 2721  df-rmo 2722
This theorem is referenced by:  reuind  3218  oawordeulem  7210  fin23lem23  8707  nqereu  9305  receu  10208  lbreu  10507  cju  10556  fprodser  13946  divalglem9  14324  divalglem9OLD  14325  ndvdssub  14331  qredeu  14607  pj1eu  17289  efgredeu  17345  lspsneu  18289  qtopeu  20673  qtophmeo  20774  minveclem7  22319  minveclem7OLD  22331  ig1peu  23064  ig1peuOLD  23065  coeeu  23121  plydivalg  23194  hlcgreu  24605  mirreu3  24641  trgcopyeu  24790  axcontlem2  24937  usgra2edg1  25052  usgraedgreu  25057  nbgraf1olem1  25111  4cycl2vnunb  25687  frg2wot1  25727  exidu1  25996  rngoideu  26054  minvecolem7  26467  minvecolem7OLD  26477  hlimreui  26834  riesz4i  27658  cdjreui  28027  xreceu  28342  cvmseu  29951  nocvxmin  30529  segconeu  30727  outsideofeu  30847  poimirlem4  31851  bfp  32063  lshpsmreu  32587  cdleme  34039  lcfl7N  34981  mapdpg  35186  hdmap14lem6  35356  mpaaeu  35929  icceuelpart  38563  usgr2edg1  39041  usgredgreu  39045  usgredg2vtxeu  39047  usgvincvadeu  39308  usgvincvadeuALT  39311  usg2edgneu  39315
  Copyright terms: Public domain W3C validator