Theorem nel02

Description: The empty set has no elements. (Contributed by Peter Mazsa, 4-Jan-2018)

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

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$$