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

Theorem reu4 2972
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 2766 . 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 2971 . . 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 2556   E.wrex 2557   E!wreu 2558   E*wrmo 2559
This theorem is referenced by:  reuind  2981  oawordeulem  6568  fin23lem23  7968  nqereu  8569  receu  9429  lbreu  9720  cju  9758  divalglem9  12616  ndvdssub  12622  qredeu  12802  pj1eu  15021  efgredeu  15077  lspsneu  15892  qtopeu  17423  qtophmeo  17524  minveclem7  18815  ig1peu  19573  coeeu  19623  plydivalg  19695  exidu1  21009  rngoideu  21067  minvecolem7  21478  hlimreui  21835  riesz4i  22659  cdjreui  23028  xreceu  23121  cvmseu  23822  nocvxmin  24416  axcontlem2  24665  segconeu  24706  outsideofeu  24826  negveud  25771  negveudr  25772  bfp  26651  mpaaeu  27458  4cycl2vnunb  28439  lshpsmreu  29921  cdleme  31371  lcfl7N  32313  mapdpg  32518  hdmap14lem6  32688
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-cleq 2289  df-clel 2292  df-ral 2561  df-rex 2562  df-reu 2563  df-rmo 2564
  Copyright terms: Public domain W3C validator