Definition df-1o 6562

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 6555	. 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  6569  df1o2  6575  ordgt0ge1  6581  oa1suc  6613  1onn  6666  nnm1  6671  nlt1pig  7528  indpi  7529  1tonninf  10663  hash1  11033  012of  16357  2o01f  16358  pwle2  16364  isomninnlem  16398  iswomninnlem  16417  ismkvnnlem  16420