Definition df-1o 6649

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 6642	. 2 class 1o
2		c0 3510	. . 3 class (/)
3	2	csuc 4488	. 2 class suc (/)
4	1, 3	wceq 1398	1 wff 1o = suc (/)

This definition is referenced by:  1on  6656  df1o2  6663  ordgt0ge1  6670  oa1suc  6702  1onn  6755  nnm1  6760  nlt1pig  7658  indpi  7659  1tonninf  10807  hash1  11180  012of  16784  2o01f  16785  pwle2  16789  isomninnlem  16831  iswomninnlem  16851  ismkvnnlem  16854