Definition df-1o 6483

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

Assertion

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

Detailed syntax breakdown of Definition df-1o

Step	Hyp	Ref	Expression
1		c1o 6476	. 2 class 1o
2		c0 3451	. . 3 class ∅
3	2	csuc 4401	. 2 class suc ∅
4	1, 3	wceq 1364	1 wff 1o = suc ∅

This definition is referenced by:  1on  6490  df1o2  6496  ordgt0ge1  6502  oa1suc  6534  1onn  6587  nnm1  6592  nlt1pig  7425  indpi  7426  1tonninf  10550  hash1  10920  012of  15724  2o01f  15725  pwle2  15729  isomninnlem  15761  iswomninnlem  15780  ismkvnnlem  15783