Definition df-2o 6385

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 6378	. 2 class 2o
2		c1o 6377	. . 3 class 1o
3	2	csuc 4343	. 2 class suc 1o
4	1, 3	wceq 1343	1 wff 2o = suc 1o

This definition is referenced by:  2on  6393  2on0  6394  df2o3  6398  o1p1e2  6436  2onn  6489  nnm2  6493  enpr2d  6783  snnen2og  6825  1nen2  6827  pm54.43  7146  en2eleq  7151  en2other2  7152  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  prarloclemarch2  7360  prarloclemlt  7434  prarloclemn  7440  hash2  10725  bj-el2oss1o  13655  pwle2  13878  nnsf  13885