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

Theorem rexex 2615
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 2562 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
2 simpr 447 . . 3  |-  ( ( x  e.  A  /\  ph )  ->  ph )
32eximi 1566 . 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 1531    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  reu3  2968  rmo2i  3090  dffo5  5693  nqerf  8570  supsrlem  8749  vdwmc2  13042  isch3  21837  19.9d2rf  23198  19.9d2r  23199  dfrdg4  24560  aline  26177  stoweidlem57  27909  bnj594  29260  bnj1371  29375  bnj1374  29377
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-rex 2562
  Copyright terms: Public domain W3C validator