Definition df-1o 6419

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 6412	. 2 class 1o
2		c0 3424	. . 3 class ∅
3	2	csuc 4367	. 2 class suc ∅
4	1, 3	wceq 1353	1 wff 1o = suc ∅

This definition is referenced by:  1on  6426  df1o2  6432  ordgt0ge1  6438  oa1suc  6470  1onn  6523  nnm1  6528  nlt1pig  7342  indpi  7343  1tonninf  10442  hash1  10793  012of  14784  2o01f  14785  pwle2  14787  isomninnlem  14817  iswomninnlem  14836  ismkvnnlem  14839