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	$$⊢\phi \to \forall !x\in A\psi$$
Assertion	alscn0d	$$⊢\phi \to A\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		alscn0d.1	$$⊢\phi \to \forall !x\in A\psi$$
2	1	alsc2d	$$⊢\phi \to \exists xx\in A$$
3		n0	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$
4	2 3	sylibr	$$⊢\phi \to A\ne \varnothing$$