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

Theorem rexex 2602
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 2549 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
2 simpr 447 . . 3  |-  ( ( x  e.  A  /\  ph )  ->  ph )
32eximi 1563 . 2  |-  ( E. x ( x  e.  A  /\  ph )  ->  E. x ph )
41, 3sylbi 187 1  |-  ( E. x  e.  A  ph  ->  E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1528    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  reu3  2955  rmo2i  3077  dffo5  5677  nqerf  8554  supsrlem  8733  vdwmc2  13026  isch3  21821  19.9d2rf  23182  19.9d2r  23183  dfrdg4  24488  aline  26074  stoweidlem57  27806  bnj594  28944  bnj1371  29059  bnj1374  29061
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-rex 2549
  Copyright terms: Public domain W3C validator