Theorem onn0

Description: The class of all ordinal numbers is not empty. (Contributed by NM, 17-Sep-1995)

	Ref	Expression
Assertion	onn0	$$⊢\mathrm{On}\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0elon	$$⊢\varnothing \in \mathrm{On}$$
2	1	ne0ii	$$⊢\mathrm{On}\ne \varnothing$$