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

Theorem reu4 3290
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 3070 . 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 3289 . . 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 2807   E.wrex 2808   E!wreu 2809   E*wrmo 2810
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-cleq 2452  df-clel 2455  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815
This theorem is referenced by:  reuind  3300  oawordeulem  7193  fin23lem23  8695  nqereu  9296  receu  10183  lbreu  10482  cju  10521  divalglem9  13907  ndvdssub  13913  qredeu  14096  pj1eu  16503  efgredeu  16559  lspsneu  17545  qtopeu  19945  qtophmeo  20046  minveclem7  21578  ig1peu  22300  coeeu  22350  plydivalg  22422  mirreu3  23741  axcontlem2  23937  usgra2edg1  24045  usgraedgreu  24050  nbgraf1olem1  24103  exidu1  24854  rngoideu  24912  minvecolem7  25325  hlimreui  25683  riesz4i  26508  cdjreui  26877  xreceu  27136  cvmseu  28211  fprodser  28508  nocvxmin  28878  segconeu  29088  outsideofeu  29208  bfp  29774  mpaaeu  30557  usgvincvadeu  31671  usgvincvadeuALT  31674  usg2edgneu  31678  4cycl2vnunb  31735  frg2wot1  31776  lshpsmreu  33781  cdleme  35231  lcfl7N  36173  mapdpg  36378  hdmap14lem6  36548
  Copyright terms: Public domain W3C validator