Definition df-2o 6692

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 6685	. 2 class 2o
2		c1o 6684	. . 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  6700  2on0  6701  df2o3  6706  o1p1e2  6745  2onn  6798  nnm2  6803  enpr2d  7115  snnen2og  7164  1nen2  7166  pm54.43  7542  en2eleq  7553  en2other2  7554  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  prarloclemarch2  7792  prarloclemlt  7866  prarloclemn  7872  hash2  11275  bj-el2oss1o  17007  pwle2  17233  nnsf  17254