Definition df-1o 6395

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 6388	. 2 class 1o
2		c0 3414	. . 3 class ∅
3	2	csuc 4350	. 2 class suc ∅
4	1, 3	wceq 1348	1 wff 1o = suc ∅

This definition is referenced by:  1on  6402  df1o2  6408  ordgt0ge1  6414  oa1suc  6446  1onn  6499  nnm1  6504  nlt1pig  7303  indpi  7304  1tonninf  10396  hash1  10746  012of  14028  2o01f  14029  pwle2  14031  isomninnlem  14062  iswomninnlem  14081  ismkvnnlem  14084