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

Theorem reu4 3129
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 2922 . 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 3128 . . 3  |-  ( E* x  e.  A ph  <->  A. x  e.  A  A. y  e.  A  (
( ph  /\  ps )  ->  x  =  y ) )
43anbi2i 677 . 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 242 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 178    /\ wa 360   A.wral 2706   E.wrex 2707   E!wreu 2708   E*wrmo 2709
This theorem is referenced by:  reuind  3138  oawordeulem  6798  fin23lem23  8207  nqereu  8807  receu  9668  lbreu  9959  cju  9997  divalglem9  12922  ndvdssub  12928  qredeu  13108  pj1eu  15329  efgredeu  15385  lspsneu  16196  qtopeu  17749  qtophmeo  17850  minveclem7  19337  ig1peu  20095  coeeu  20145  plydivalg  20217  usgra2edg1  21404  usgraedgreu  21408  nbgraf1olem1  21452  exidu1  21915  rngoideu  21973  minvecolem7  22386  hlimreui  22743  riesz4i  23567  cdjreui  23936  xreceu  24169  cvmseu  24964  fprodser  25276  nocvxmin  25647  axcontlem2  25905  segconeu  25946  outsideofeu  26066  bfp  26534  mpaaeu  27333  4cycl2vnunb  28408  frg2wot1  28447  lshpsmreu  29908  cdleme  31358  lcfl7N  32300  mapdpg  32505  hdmap14lem6  32675
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-cleq 2430  df-clel 2433  df-ral 2711  df-rex 2712  df-reu 2713  df-rmo 2714
  Copyright terms: Public domain W3C validator