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		noel	$$⊢\neg B\in \varnothing$$
2		eleq2	$$⊢A=\varnothing \to \left(B\in A\leftrightarrow B\in \varnothing \right)$$
3	1 2	mtbiri	$$⊢A=\varnothing \to \neg B\in A$$
4	3	con2i	$$⊢B\in A\to \neg A=\varnothing$$