Definition df-1o 6660

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 6653	. 2 class 1o
2		c0 3512	. . 3 class ∅
3	2	csuc 4491	. 2 class suc ∅
4	1, 3	wceq 1398	1 wff 1o = suc ∅

This definition is referenced by:  1on  6667  df1o2  6674  ordgt0ge1  6681  oa1suc  6713  1onn  6766  nnm1  6771  nlt1pig  7672  indpi  7673  1tonninf  10830  hash1  11204  012of  16907  2o01f  16908  pwle2  16912  isomninnlem  16954  iswomninnlem  16974  ismkvnnlem  16977