Metamath Proof Explorer

Theorem rexex

Description: Restricted existence implies existence. (Contributed by NM, 11-Nov-1995)

Ref Expression
Assertion rexex 
|- ( E. x e. A ph -> E. x ph )

Proof

Step Hyp Ref Expression
1 df-rex 
 |-  ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
2 exsimpr 
 |-  ( E. x ( x e. A /\ ph ) -> E. x ph )
3 1 2 sylbi 
 |-  ( E. x e. A ph -> E. x ph )