Definition df-1o 6585

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 6578	. 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  6592  df1o2  6599  ordgt0ge1  6606  oa1suc  6638  1onn  6691  nnm1  6696  nlt1pig  7564  indpi  7565  1tonninf  10707  hash1  11079  012of  16651  2o01f  16652  pwle2  16658  isomninnlem  16693  iswomninnlem  16713  ismkvnnlem  16716