Definition df-1o 6407

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

This definition is referenced by:  1on  6414  df1o2  6420  ordgt0ge1  6426  oa1suc  6458  1onn  6511  nnm1  6516  nlt1pig  7315  indpi  7316  1tonninf  10408  hash1  10757  012of  14303  2o01f  14304  pwle2  14306  isomninnlem  14337  iswomninnlem  14356  ismkvnnlem  14359