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

Theorem reurex 3037
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 3036 . 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 2797   E!wreu 2798   E*wrmo 2799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-eu 2265  df-mo 2266  df-rex 2802  df-reu 2803  df-rmo 2804
This theorem is referenced by:  reu3  3250  sbcreu  3375  reusv7OLD  4607  reuxfrd  4620  weniso  6149  oawordex  7101  oaabs  7188  oaabs2  7189  supval2  7811  fisup2g  7822  nqerf  9205  qbtwnre  11275  modprm0  13986  meet0  15421  join0  15422  issrgid  16741  isrngid  16788  lspsneu  17322  frgpcyg  18126  qtophmeo  19517  pjthlem2  21052  dyadmax  21206  quotlem  21894  pjhthlem2  24942  cnlnadj  25630  reuxfr4d  26021  rmoxfrdOLD  26023  rmoxfrd  26024  cvmliftpht  27346  tz6.26  27805  2reu2rex  30150  2rexreu  30152  2reu4  30157  frgra2v  30734  2pthfrgrarn  30744  frgrancvvdeqlemC  30775  frg2wotn0  30792  lcfl7N  35465
  Copyright terms: Public domain W3C validator