Definition df-2o 6693

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 6686	. 2 class 2o
2		c1o 6685	. . 3 class 1o
3	2	csuc 4512	. 2 class suc 1o
4	1, 3	wceq 1402	1 wff 2o = suc 1o

This definition is used by:  2on  6701  2on0  6702  df2o3  6707  o1p1e2  6746  2onn  6799  nnm2  6804  enpr2d  7117  snnen2og  7166  1nen2  7168  pm54.43  7542  en2eleq  7553  en2other2  7554  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  prarloclemarch2  7792  prarloclemlt  7866  prarloclemn  7872  hash2  11274  bj-el2oss1o  17024  pwle2  17250  nnsf  17271