Metamath Proof Explorer

Theorem alscn0d

Description: Deduction rule: Given "all some" applied to a class, the class is not the empty set. (Contributed by David A. Wheeler, 23-Oct-2018)

Ref Expression
Hypothesis alscn0d.1 
|- ( ph -> A! x e. A ps )
Assertion alscn0d 
|- ( ph -> A =/= (/) )

Proof

Step Hyp Ref Expression
1 alscn0d.1 
 |-  ( ph -> A! x e. A ps )
2 1 alsc2d 
 |-  ( ph -> E. x x e. A )
3 n0 
 |-  ( A =/= (/) <-> E. x x e. A )
4 2 3 sylibr 
 |-  ( ph -> A =/= (/) )