Theorem 0elon

Description: The empty set is an ordinal number. Corollary 7N(b) of Enderton p. 193. Remark 1.5 of Schloeder p. 1. (Contributed by NM, 17-Sep-1993)

	Ref	Expression
Assertion	0elon	⊢ ∅ ∈ On

Proof

Step	Hyp	Ref	Expression
1		ord0	⊢ Ord ∅
2		0ex	⊢ ∅ ∈ V
3	2	elon	⊢ ( ∅ ∈ On ↔ Ord ∅ )
4	1 3	mpbir	⊢ ∅ ∈ On