Definition df-1o 6502

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

This definition is referenced by:  1on  6509  df1o2  6515  ordgt0ge1  6521  oa1suc  6553  1onn  6606  nnm1  6611  nlt1pig  7454  indpi  7455  1tonninf  10586  hash1  10956  012of  15934  2o01f  15935  pwle2  15939  isomninnlem  15973  iswomninnlem  15992  ismkvnnlem  15995