Definition df-1o 6581

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 6574	. 2 class 1o
2		c0 3494	. . 3 class (/)
3	2	csuc 4462	. 2 class suc (/)
4	1, 3	wceq 1397	1 wff 1o = suc (/)

This definition is referenced by:  1on  6588  df1o2  6595  ordgt0ge1  6602  oa1suc  6634  1onn  6687  nnm1  6692  nlt1pig  7560  indpi  7561  1tonninf  10702  hash1  11074  012of  16592  2o01f  16593  pwle2  16599  isomninnlem  16634  iswomninnlem  16653  ismkvnnlem  16656