Metamath Proof Explorer

Theorem rexn0

Description: Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007)

Ref Expression
Assertion rexn0 
|- ( E. x e. A ph -> A =/= (/) )

Proof

Step Hyp Ref Expression
1 ne0i 
 |-  ( x e. A -> A =/= (/) )
2 1 a1d 
 |-  ( x e. A -> ( ph -> A =/= (/) ) )
3 2 rexlimiv 
 |-  ( E. x e. A ph -> A =/= (/) )