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

Theorem reurex 3078
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 3077 . 2  |-  ( E! x  e.  A  ph  <->  ( E. x  e.  A  ph 
/\  E* x  e.  A  ph ) )
21simplbi 460 1  |-  ( E! x  e.  A  ph  ->  E. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wrex 2815   E!wreu 2816   E*wrmo 2817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-eu 2279  df-mo 2280  df-rex 2820  df-reu 2821  df-rmo 2822
This theorem is referenced by:  reu3  3293  sbcreu  3418  reusv7OLD  4659  reuxfrd  4672  weniso  6238  oawordex  7206  oaabs  7293  oaabs2  7294  supval2  7915  fisup2g  7926  nqerf  9308  qbtwnre  11398  modprm0  14189  meet0  15624  join0  15625  issrgid  16976  isrngid  17025  lspsneu  17569  frgpcyg  18407  qtophmeo  20081  pjthlem2  21616  dyadmax  21770  quotlem  22458  frgra2v  24703  2pthfrgrarn  24713  frgrancvvdeqlemC  24744  frg2wotn0  24761  pjhthlem2  26014  cnlnadj  26702  reuxfr4d  27093  rmoxfrdOLD  27095  rmoxfrd  27096  cvmliftpht  28431  tz6.26  28890  2reu2rex  31683  2rexreu  31685  2reu4  31690  lcfl7N  36316
  Copyright terms: Public domain W3C validator