Definition df-1o 6474

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 6467	. 2 class 1o
2		c0 3450	. . 3 class (/)
3	2	csuc 4400	. 2 class suc (/)
4	1, 3	wceq 1364	1 wff 1o = suc (/)

This definition is referenced by:  1on  6481  df1o2  6487  ordgt0ge1  6493  oa1suc  6525  1onn  6578  nnm1  6583  nlt1pig  7408  indpi  7409  1tonninf  10533  hash1  10903  012of  15640  2o01f  15641  pwle2  15643  isomninnlem  15674  iswomninnlem  15693  ismkvnnlem  15696