Metamath Proof Explorer

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