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  10827  hash1  11201  012of  16893  2o01f  16894  pwle2  16898  isomninnlem  16940  iswomninnlem  16960  ismkvnnlem  16963