Definition df-2o 6408

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 6401	. 2 class 2o
2		c1o 6400	. . 3 class 1o
3	2	csuc 4359	. 2 class suc 1o
4	1, 3	wceq 1353	1 wff 2o = suc 1o

This definition is referenced by:  2on  6416  2on0  6417  df2o3  6421  o1p1e2  6459  2onn  6512  nnm2  6517  enpr2d  6807  snnen2og  6849  1nen2  6851  pm54.43  7179  en2eleq  7184  en2other2  7185  exmidfodomrlemr  7191  exmidfodomrlemrALT  7192  prarloclemarch2  7393  prarloclemlt  7467  prarloclemn  7473  hash2  10760  bj-el2oss1o  14095  pwle2  14317  nnsf  14324