Definition df-1o 6365

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 6358	. 2 class 1o
2		c0 3395	. . 3 class (/)
3	2	csuc 4327	. 2 class suc (/)
4	1, 3	wceq 1335	1 wff 1o = suc (/)

This definition is referenced by:  1on  6372  df1o2  6378  ordgt0ge1  6384  oa1suc  6416  1onn  6469  nnm1  6473  nlt1pig  7263  indpi  7264  1tonninf  10348  hash1  10696  012of  13638  2o01f  13639  pwle2  13641  isomninnlem  13672  iswomninnlem  13691  ismkvnnlem  13694