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

Theorem rexex 2767
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 2713 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
2 exsimpr 1647 . 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 1591    e. wcel 1757   E.wrex 2708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-rex 2713
This theorem is referenced by:  reu3  3140  rmo2i  3274  dffo5  5850  nqerf  9089  supsrlem  9268  vdwmc2  14025  isch3  24469  19.9d2rf  25687  volfiniune  26502  dfrdg4  27830  mblfinlem3  28276  mblfinlem4  28277  stoweidlem57  29700  bnj594  31647  bnj1371  31762  bnj1374  31764  bj-0nelsngl  32087  bj-ccinftydisj  32156
  Copyright terms: Public domain W3C validator