Definition df-2o 6626

Description: Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.)

Assertion

Ref	Expression
df-2o	|- 2o = suc 1o

Detailed syntax breakdown of Definition df-2o

Step	Hyp	Ref	Expression
1		c2o 6619	. 2 class 2o
2		c1o 6618	. . 3 class 1o
3	2	csuc 4468	. 2 class suc 1o
4	1, 3	wceq 1398	1 wff 2o = suc 1o

This definition is referenced by:  2on  6634  2on0  6635  df2o3  6640  o1p1e2  6679  2onn  6732  nnm2  6737  enpr2d  7040  snnen2og  7088  1nen2  7090  pm54.43  7455  en2eleq  7466  en2other2  7467  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  prarloclemarch2  7699  prarloclemlt  7773  prarloclemn  7779  hash2  11139  bj-el2oss1o  16492  pwle2  16720  nnsf  16731