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 =/= (/)