Metamath Proof Explorer


Theorem onn0

Description: The class of all ordinal numbers is not empty. (Contributed by NM, 17-Sep-1995)

Ref Expression
Assertion onn0
|- On =/= (/)

Proof

Step Hyp Ref Expression
1 0elon
 |-  (/) e. On
2 1 ne0ii
 |-  On =/= (/)