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

Theorem rexex 2710
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 2657 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
2 simpr 448 . . 3  |-  ( ( x  e.  A  /\  ph )  ->  ph )
32eximi 1582 . 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 1547    e. wcel 1717   E.wrex 2652
This theorem is referenced by:  reu3  3069  rmo2i  3192  dffo5  5827  nqerf  8742  supsrlem  8921  vdwmc2  13276  isch3  22594  19.9d2rf  23814  volfiniune  24382  dfrdg4  25515  stoweidlem57  27476  bnj594  28623  bnj1371  28738  bnj1374  28740
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-rex 2657
  Copyright terms: Public domain W3C validator