Definition df-1o 6568

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 6561	. 2 class 1o
2		c0 3491	. . 3 class (/)
3	2	csuc 4456	. 2 class suc (/)
4	1, 3	wceq 1395	1 wff 1o = suc (/)

This definition is referenced by:  1on  6575  df1o2  6582  ordgt0ge1  6589  oa1suc  6621  1onn  6674  nnm1  6679  nlt1pig  7539  indpi  7540  1tonninf  10675  hash1  11046  012of  16444  2o01f  16445  pwle2  16451  isomninnlem  16486  iswomninnlem  16505  ismkvnnlem  16508