Definition df-1o 6442

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 6435	. 2 class 1o
2		c0 3437	. . 3 class (/)
3	2	csuc 4383	. 2 class suc (/)
4	1, 3	wceq 1364	1 wff 1o = suc (/)

This definition is referenced by:  1on  6449  df1o2  6455  ordgt0ge1  6461  oa1suc  6493  1onn  6546  nnm1  6551  nlt1pig  7371  indpi  7372  1tonninf  10473  hash1  10826  012of  15224  2o01f  15225  pwle2  15227  isomninnlem  15257  iswomninnlem  15276  ismkvnnlem  15279