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

Theorem rexex 2757
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 2703 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
2 simpr 448 . . 3  |-  ( ( x  e.  A  /\  ph )  ->  ph )
32eximi 1585 . 2  |-  ( E. x ( x  e.  A  /\  ph )  ->  E. x ph )
41, 3sylbi 188 1  |-  ( E. x  e.  A  ph  ->  E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   E.wex 1550    e. wcel 1725   E.wrex 2698
This theorem is referenced by:  reu3  3116  rmo2i  3239  dffo5  5878  nqerf  8799  supsrlem  8978  vdwmc2  13339  isch3  22736  19.9d2rf  23960  volfiniune  24578  dfrdg4  25787  mblfinlem2  26235  mblfinlem3  26236  stoweidlem57  27773  bnj594  29220  bnj1371  29335  bnj1374  29337
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-rex 2703
  Copyright terms: Public domain W3C validator