Definition df-2o 6505

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 6498	. 2 class 2o
2		c1o 6497	. . 3 class 1o
3	2	csuc 4413	. 2 class suc 1o
4	1, 3	wceq 1373	1 wff 2o = suc 1o

This definition is referenced by:  2on  6513  2on0  6514  df2o3  6518  o1p1e2  6556  2onn  6609  nnm2  6614  enpr2d  6913  snnen2og  6958  1nen2  6960  pm54.43  7300  en2eleq  7305  en2other2  7306  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  prarloclemarch2  7534  prarloclemlt  7608  prarloclemn  7614  hash2  10959  bj-el2oss1o  15747  pwle2  15972  nnsf  15979