Definition df-2o 6516

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 6509	. 2 class 2o
2		c1o 6508	. . 3 class 1o
3	2	csuc 4420	. 2 class suc 1o
4	1, 3	wceq 1373	1 wff 2o = suc 1o

This definition is referenced by:  2on  6524  2on0  6525  df2o3  6529  o1p1e2  6567  2onn  6620  nnm2  6625  enpr2d  6925  snnen2og  6971  1nen2  6973  pm54.43  7313  en2eleq  7319  en2other2  7320  exmidfodomrlemr  7326  exmidfodomrlemrALT  7327  prarloclemarch2  7552  prarloclemlt  7626  prarloclemn  7632  hash2  10979  bj-el2oss1o  15849  pwle2  16076  nnsf  16083