Theorem ne0i

Description: If a class has elements, then it is nonempty. (Contributed by NM, 31-Dec-1993)

	Ref	Expression
Assertion	ne0i	$$⊢B\in A\to A\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		n0i	$$⊢B\in A\to \neg A=\varnothing$$
2	1	neqned	$$⊢B\in A\to A\ne \varnothing$$