Definition df-2o 6503

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 6496	. 2 class 2o
2		c1o 6495	. . 3 class 1o
3	2	csuc 4412	. 2 class suc 1o
4	1, 3	wceq 1373	1 wff 2o = suc 1o

This definition is referenced by:  2on  6511  2on0  6512  df2o3  6516  o1p1e2  6554  2onn  6607  nnm2  6612  enpr2d  6911  snnen2og  6956  1nen2  6958  pm54.43  7298  en2eleq  7303  en2other2  7304  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  prarloclemarch2  7532  prarloclemlt  7606  prarloclemn  7612  hash2  10957  bj-el2oss1o  15710  pwle2  15935  nnsf  15942