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

Theorem reurex 2914
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 2913 . 2  |-  ( E! x  e.  A  ph  <->  ( E. x  e.  A  ph 
/\  E* x  e.  A ph ) )
21simplbi 447 1  |-  ( E! x  e.  A  ph  ->  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wrex 2698   E!wreu 2699   E*wrmo 2700
This theorem is referenced by:  reu3  3116  reusv7OLD  4727  reuxfrd  4740  weniso  6067  oawordex  6792  oaabs  6879  oaabs2  6880  fisup2g  7463  nqerf  8799  qbtwnre  10777  spwex  14653  isrngid  15681  lspsneu  16187  frgpcyg  16846  qtophmeo  17841  pjthlem2  19331  dyadmax  19482  quotlem  20209  pjhthlem2  22886  cnlnadj  23574  reuxfr4d  23969  rmoxfrdOLD  23971  rmoxfrd  23972  subofld  24237  cvmliftpht  24997  tz6.26  25472  2reu2rex  27928  2rexreu  27930  2reu4  27935  modprm0  28194  2pthfrgrarn  28336  frgrancvvdeqlemC  28365  frg2wotn0  28382  lcfl7N  32236
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-rex 2703  df-reu 2704  df-rmo 2705
  Copyright terms: Public domain W3C validator