Theorem on0eln0

Description: An ordinal number contains zero iff it is nonzero. (Contributed by NM, 6-Dec-2004)

	Ref	Expression
Assertion	on0eln0	$$⊢A\in \mathrm{On}\to \left(\varnothing \in A\leftrightarrow A\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		eloni	$$⊢A\in \mathrm{On}\to \mathrm{Ord}A$$
2		ord0eln0	$$⊢\mathrm{Ord}A\to \left(\varnothing \in A\leftrightarrow A\ne \varnothing \right)$$
3	1 2	syl	$$⊢A\in \mathrm{On}\to \left(\varnothing \in A\leftrightarrow A\ne \varnothing \right)$$