Metamath Proof Explorer


Theorem reximdva0

Description: Restricted existence deduced from nonempty class. (Contributed by NM, 1-Feb-2012)

Ref Expression
Hypothesis reximdva0.1
|- ( ( ph /\ x e. A ) -> ps )
Assertion reximdva0
|- ( ( ph /\ A =/= (/) ) -> E. x e. A ps )

Proof

Step Hyp Ref Expression
1 reximdva0.1
 |-  ( ( ph /\ x e. A ) -> ps )
2 n0
 |-  ( A =/= (/) <-> E. x x e. A )
3 1 ex
 |-  ( ph -> ( x e. A -> ps ) )
4 3 ancld
 |-  ( ph -> ( x e. A -> ( x e. A /\ ps ) ) )
5 4 eximdv
 |-  ( ph -> ( E. x x e. A -> E. x ( x e. A /\ ps ) ) )
6 5 imp
 |-  ( ( ph /\ E. x x e. A ) -> E. x ( x e. A /\ ps ) )
7 2 6 sylan2b
 |-  ( ( ph /\ A =/= (/) ) -> E. x ( x e. A /\ ps ) )
8 df-rex
 |-  ( E. x e. A ps <-> E. x ( x e. A /\ ps ) )
9 7 8 sylibr
 |-  ( ( ph /\ A =/= (/) ) -> E. x e. A ps )