Definition df-1o 6380

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 6373	. 2 class 1o
2		c0 3408	. . 3 class (/)
3	2	csuc 4342	. 2 class suc (/)
4	1, 3	wceq 1343	1 wff 1o = suc (/)

This definition is referenced by:  1on  6387  df1o2  6393  ordgt0ge1  6399  oa1suc  6431  1onn  6484  nnm1  6488  nlt1pig  7278  indpi  7279  1tonninf  10371  hash1  10720  012of  13835  2o01f  13836  pwle2  13838  isomninnlem  13869  iswomninnlem  13888  ismkvnnlem  13891