Definition df-1o 6504

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

This definition is referenced by:  1on  6511  df1o2  6517  ordgt0ge1  6523  oa1suc  6555  1onn  6608  nnm1  6613  nlt1pig  7456  indpi  7457  1tonninf  10588  hash1  10958  012of  15967  2o01f  15968  pwle2  15972  isomninnlem  16006  iswomninnlem  16025  ismkvnnlem  16028