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

Theorem reurex 2924
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 2923 . 2  |-  ( E! x  e.  A  ph  <->  ( E. x  e.  A  ph 
/\  E* x  e.  A ph ) )
21simplbi 448 1  |-  ( E! x  e.  A  ph  ->  E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wrex 2708   E!wreu 2709   E*wrmo 2710
This theorem is referenced by:  reu3  3126  reusv7OLD  4738  reuxfrd  4751  weniso  6078  oawordex  6803  oaabs  6890  oaabs2  6891  fisup2g  7474  nqerf  8812  qbtwnre  10790  spwex  14666  isrngid  15694  lspsneu  16200  frgpcyg  16859  qtophmeo  17854  pjthlem2  19344  dyadmax  19495  quotlem  20222  pjhthlem2  22899  cnlnadj  23587  reuxfr4d  23982  rmoxfrdOLD  23984  rmoxfrd  23985  subofld  24250  cvmliftpht  25010  tz6.26  25485  2reu2rex  27951  2rexreu  27953  2reu4  27958  modprm0  28262  2pthfrgrarn  28473  frgrancvvdeqlemC  28502  frg2wotn0  28519  lcfl7N  32373
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-rex 2713  df-reu 2714  df-rmo 2715
  Copyright terms: Public domain W3C validator