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

Theorem reurex 3052
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 3051 . 2  |-  ( E! x  e.  A  ph  <->  ( E. x  e.  A  ph 
/\  E* x  e.  A  ph ) )
21simplbi 461 1  |-  ( E! x  e.  A  ph  ->  E. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wrex 2783   E!wreu 2784   E*wrmo 2785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-eu 2270  df-mo 2271  df-rex 2788  df-reu 2789  df-rmo 2790
This theorem is referenced by:  reu3  3267  sbcreu  3382  reuxfrd  4647  tz6.26  5430  weniso  6260  oawordex  7266  oaabs  7353  oaabs2  7354  supval2  7975  fisup2g  7990  nqerf  9354  qbtwnre  11492  modprm0  14719  meet0  16334  join0  16335  issrgid  17691  isringid  17741  lspsneu  18281  frgpcyg  19075  qtophmeo  20763  pjthlem2  22273  dyadmax  22433  quotlem  23121  frgra2v  25572  2pthfrgrarn  25582  frgrancvvdeqlemC  25612  frg2wotn0  25629  pjhthlem2  26880  cnlnadj  27567  reuxfr4d  27961  rmoxfrdOLD  27963  rmoxfrd  27964  cvmliftpht  29829  lcfl7N  34781  2reu2rex  38007  2rexreu  38009  2reu4  38014  isringrng  38651  uzlidlring  38699
  Copyright terms: Public domain W3C validator