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

Theorem reu4 3250
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 3032 . 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 3249 . . 3  |-  ( E* x  e.  A  ph  <->  A. x  e.  A  A. y  e.  A  (
( ph  /\  ps )  ->  x  =  y ) )
43anbi2i 694 . 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 249 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 184    /\ wa 369   A.wral 2795   E.wrex 2796   E!wreu 2797   E*wrmo 2798
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-cleq 2443  df-clel 2446  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803
This theorem is referenced by:  reuind  3260  oawordeulem  7093  fin23lem23  8596  nqereu  9199  receu  10082  lbreu  10381  cju  10419  divalglem9  13707  ndvdssub  13713  qredeu  13895  pj1eu  16297  efgredeu  16353  lspsneu  17310  qtopeu  19405  qtophmeo  19506  minveclem7  21038  ig1peu  21759  coeeu  21809  plydivalg  21881  mirreu3  23184  axcontlem2  23346  usgra2edg1  23437  usgraedgreu  23441  nbgraf1olem1  23485  exidu1  23948  rngoideu  24006  minvecolem7  24419  hlimreui  24777  riesz4i  25602  cdjreui  25971  xreceu  26231  cvmseu  27299  fprodser  27596  nocvxmin  27966  segconeu  28176  outsideofeu  28296  bfp  28861  mpaaeu  29645  4cycl2vnunb  30747  frg2wot1  30788  lshpsmreu  33060  cdleme  34510  lcfl7N  35452  mapdpg  35657  hdmap14lem6  35827
  Copyright terms: Public domain W3C validator