Metamath Proof Explorer


Theorem 0elon

Description: The empty set is an ordinal number. Corollary 7N(b) of Enderton p. 193. (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