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