Metamath Proof Explorer

Theorem ord0

Description: The empty set is an ordinal class. (Contributed by NM, 11-May-1994)

Ref Expression
Assertion ord0 ⊢ Ord ⁡ ∅

Proof

Step Hyp Ref Expression
1 tr0 ⊢ Tr ⁡ ∅
2 we0 ⊢ E We ∅
3 df-ord ⊢ Ord ⁡ ∅ ↔ Tr ⁡ ∅ ∧ E We ∅
4 1 2 3 mpbir2an ⊢ Ord ⁡ ∅