Definition df-1o 6416

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 6409	. 2 class 1o
2		c0 3422	. . 3 class (/)
3	2	csuc 4365	. 2 class suc (/)
4	1, 3	wceq 1353	1 wff 1o = suc (/)

This definition is referenced by:  1on  6423  df1o2  6429  ordgt0ge1  6435  oa1suc  6467  1onn  6520  nnm1  6525  nlt1pig  7339  indpi  7340  1tonninf  10439  hash1  10790  012of  14715  2o01f  14716  pwle2  14718  isomninnlem  14748  iswomninnlem  14767  ismkvnnlem  14770