Definition df-1o 6691

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 6684	. 2 class 1o
2		c0 3520	. . 3 class (/)
3	2	csuc 4512	. 2 class suc (/)
4	1, 3	wceq 1402	1 wff 1o = suc (/)

This definition is used by:  1on  6698  df1o2  6705  ordgt0ge1  6712  oa1suc  6744  1onn  6797  nnm1  6802  nlt1pig  7714  indpi  7715  1tonninf  10899  hash1  11274  012of  17228  2o01f  17229  pwle2  17233  isomninnlem  17285  iswomninnlem  17306  ismkvnnlem  17309