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

Theorem reurex 2754
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 2753 . 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 2544   E!wreu 2545   E*wrmo 2546
This theorem is referenced by:  reu3  2955  reusv7OLD  4546  reuxfrd  4559  weniso  5852  oawordex  6555  oaabs  6642  oaabs2  6643  fisup2g  7217  fisupcl  7218  nqerf  8554  qbtwnre  10526  spwex  14338  isrngid  15366  lspsneu  15876  frgpcyg  16527  qtophmeo  17508  pjthlem2  18802  dyadmax  18953  quotlem  19680  pjhthlem2  21971  cnlnadj  22659  reuxfr4d  23139  rmoxfrdOLD  23146  rmoxfrd  23147  cvmliftpht  23849  tz6.26  24205  2reu2rex  27961  2rexreu  27963  2reu4  27968  lcfl7N  31691
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-rex 2549  df-reu 2550  df-rmo 2551
  Copyright terms: Public domain W3C validator