Theorem n0i

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

	Ref	Expression
Assertion	n0i	$$⊢B\in A\to \neg A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		nel02	$$⊢A=\varnothing \to \neg B\in A$$
2	1	con2i	$$⊢B\in A\to \neg A=\varnothing$$