Definition df-2o 6136

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 6129	. 2 class 2o
2		c1o 6128	. . 3 class 1o
3	2	csuc 4166	. 2 class suc 1o
4	1, 3	wceq 1287	1 wff 2o = suc 1o

This definition is referenced by:  2on  6144  2on0  6145  df2o3  6149  o1p1e2  6183  2onn  6232  nnm2  6236  snnen2og  6527  1nen2  6529  infnninf  6749  nnnninf  6750  pm54.43  6762  en2eleq  6765  en2other2  6766  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  prarloclemarch2  6922  prarloclemlt  6996  prarloclemn  7002  hash2  10116  nnsf  11333