Definition df-1o 6512

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 6505	. 2 class 1o
2		c0 3462	. . 3 class ∅
3	2	csuc 4417	. 2 class suc ∅
4	1, 3	wceq 1373	1 wff 1o = suc ∅

This definition is referenced by:  1on  6519  df1o2  6525  ordgt0ge1  6531  oa1suc  6563  1onn  6616  nnm1  6621  nlt1pig  7467  indpi  7468  1tonninf  10599  hash1  10969  012of  16045  2o01f  16046  pwle2  16050  isomninnlem  16084  iswomninnlem  16103  ismkvnnlem  16106