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

Theorem reurex 2767
Description: Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.)
Assertion
Ref Expression
reurex  |-  ( E! x  e.  A  ph  ->  E. x  e.  A  ph )

Proof of Theorem reurex
StepHypRef Expression
1 reu5 2766 . 2  |-  ( E! x  e.  A  ph  <->  ( E. x  e.  A  ph 
/\  E* x  e.  A ph ) )
21simplbi 446 1  |-  ( E! x  e.  A  ph  ->  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wrex 2557   E!wreu 2558   E*wrmo 2559
This theorem is referenced by:  reu3  2968  reusv7OLD  4562  reuxfrd  4575  weniso  5868  oawordex  6571  oaabs  6658  oaabs2  6659  fisup2g  7233  fisupcl  7234  nqerf  8570  qbtwnre  10542  spwex  14354  isrngid  15382  lspsneu  15892  frgpcyg  16543  qtophmeo  17524  pjthlem2  18818  dyadmax  18969  quotlem  19696  pjhthlem2  21987  cnlnadj  22675  reuxfr4d  23155  rmoxfrdOLD  23162  rmoxfrd  23163  cvmliftpht  23864  tz6.26  24276  2reu2rex  28064  2rexreu  28066  2reu4  28071  2pthfrgrarn  28433  lcfl7N  32313
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
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-rex 2562  df-reu 2563  df-rmo 2564
  Copyright terms: Public domain W3C validator