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

Theorem reu4 3277
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 3057 . 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 3276 . . 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 2791   E.wrex 2792   E!wreu 2793   E*wrmo 2794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-cleq 2433  df-clel 2436  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799
This theorem is referenced by:  reuind  3287  oawordeulem  7201  fin23lem23  8704  nqereu  9305  receu  10195  lbreu  10494  cju  10533  divalglem9  13931  ndvdssub  13937  qredeu  14120  pj1eu  16583  efgredeu  16639  lspsneu  17637  qtopeu  20083  qtophmeo  20184  minveclem7  21716  ig1peu  22438  coeeu  22488  plydivalg  22560  mirreu3  23900  axcontlem2  24133  usgra2edg1  24248  usgraedgreu  24253  nbgraf1olem1  24306  4cycl2vnunb  24882  frg2wot1  24922  exidu1  25193  rngoideu  25251  minvecolem7  25664  hlimreui  26022  riesz4i  26847  cdjreui  27216  xreceu  27484  cvmseu  28587  fprodser  29049  nocvxmin  29419  segconeu  29629  outsideofeu  29749  bfp  30288  mpaaeu  31068  usgvincvadeu  32239  usgvincvadeuALT  32242  usg2edgneu  32246  lshpsmreu  34536  cdleme  35988  lcfl7N  36930  mapdpg  37135  hdmap14lem6  37305
  Copyright terms: Public domain W3C validator