Definition df-2o 6484

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 6477	. 2 class 2o
2		c1o 6476	. . 3 class 1o
3	2	csuc 4401	. 2 class suc 1o
4	1, 3	wceq 1364	1 wff 2o = suc 1o

This definition is referenced by:  2on  6492  2on0  6493  df2o3  6497  o1p1e2  6535  2onn  6588  nnm2  6593  enpr2d  6885  snnen2og  6929  1nen2  6931  pm54.43  7269  en2eleq  7274  en2other2  7275  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  prarloclemarch2  7503  prarloclemlt  7577  prarloclemn  7583  hash2  10921  bj-el2oss1o  15504  pwle2  15729  nnsf  15736