Definition df-2o 6678

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 6671	. 2 class 2o
2		c1o 6670	. . 3 class 1o
3	2	csuc 4505	. 2 class suc 1o
4	1, 3	wceq 1402	1 wff 2o = suc 1o

This definition is referenced by:  2on  6686  2on0  6687  df2o3  6692  o1p1e2  6731  2onn  6784  nnm2  6789  enpr2d  7101  snnen2og  7150  1nen2  7152  pm54.43  7526  en2eleq  7537  en2other2  7538  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  prarloclemarch2  7776  prarloclemlt  7850  prarloclemn  7856  hash2  11231  bj-el2oss1o  16716  pwle2  16942  nnsf  16953