This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ∅ ∈ On
2 1 ne0ii ⊢ On ≠ ∅