Theorem onn0

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

	Ref	Expression
Assertion	onn0	⊢ On ≠ ∅

Proof

Step	Hyp	Ref	Expression
1		0elon	⊢ ∅ ∈ On
2	1	ne0ii	⊢ On ≠ ∅