Definition df-1o 6417

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 6410	. 2 class 1o
2		c0 3423	. . 3 class (/)
3	2	csuc 4366	. 2 class suc (/)
4	1, 3	wceq 1353	1 wff 1o = suc (/)

This definition is referenced by:  1on  6424  df1o2  6430  ordgt0ge1  6436  oa1suc  6468  1onn  6521  nnm1  6526  nlt1pig  7340  indpi  7341  1tonninf  10440  hash1  10791  012of  14748  2o01f  14749  pwle2  14751  isomninnlem  14781  iswomninnlem  14800  ismkvnnlem  14803