Definition df-1o 6525

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 6518	. 2 class 1o
2		c0 3468	. . 3 class (/)
3	2	csuc 4430	. 2 class suc (/)
4	1, 3	wceq 1373	1 wff 1o = suc (/)

This definition is referenced by:  1on  6532  df1o2  6538  ordgt0ge1  6544  oa1suc  6576  1onn  6629  nnm1  6634  nlt1pig  7489  indpi  7490  1tonninf  10623  hash1  10993  012of  16130  2o01f  16131  pwle2  16137  isomninnlem  16171  iswomninnlem  16190  ismkvnnlem  16193