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 
|- (/) e. On

Proof

Step Hyp Ref Expression
1 ord0 
 |-  Ord (/)
2 0ex 
 |-  (/) e. _V
3 2 elon 
 |-  ( (/) e. On <-> Ord (/) )
4 1 3 mpbir 
 |-  (/) e. On