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

Theorem rexex 2921
Description: Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)
Assertion
Ref Expression
rexex  |-  ( E. x  e.  A  ph  ->  E. x ph )

Proof of Theorem rexex
StepHypRef Expression
1 df-rex 2820 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
2 exsimpr 1655 . 2  |-  ( E. x ( x  e.  A  /\  ph )  ->  E. x ph )
31, 2sylbi 195 1  |-  ( E. x  e.  A  ph  ->  E. x ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   E.wex 1596    e. wcel 1767   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-rex 2820
This theorem is referenced by:  reu3  3293  rmo2i  3429  dffo5  6036  nqerf  9304  supsrlem  9484  vdwmc2  14349  isch3  25832  19.9d2rf  27050  volfiniune  27839  dfrdg4  29174  mblfinlem3  29628  mblfinlem4  29629  fperdvper  31248  stoweidlem57  31357  bnj594  33049  bnj1371  33164  bnj1374  33166  bj-0nelsngl  33610  bj-ccinftydisj  33688
  Copyright terms: Public domain W3C validator