Metamath Proof Explorer


Definition df-1o

Description: Define the ordinal number 1. (Contributed by NM, 29-Oct-1995)

Ref Expression
Assertion df-1o 1o = suc ∅

Detailed syntax breakdown

Step Hyp Ref Expression
0 c1o 1o
1 c0
2 1 csuc suc ∅
3 0 2 wceq 1o = suc ∅