Definition df-1o 6680

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

This definition is referenced by:  1on  6687  df1o2  6694  ordgt0ge1  6701  oa1suc  6733  1onn  6786  nnm1  6791  nlt1pig  7701  indpi  7702  1tonninf  10859  hash1  11233  012of  16940  2o01f  16941  pwle2  16945  isomninnlem  16987  iswomninnlem  17007  ismkvnnlem  17010