Definition df-2o 6661

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 6654	. 2 class 2o
2		c1o 6653	. . 3 class 1o
3	2	csuc 4491	. 2 class suc 1o
4	1, 3	wceq 1398	1 wff 2o = suc 1o

This definition is referenced by:  2on  6669  2on0  6670  df2o3  6675  o1p1e2  6714  2onn  6767  nnm2  6772  enpr2d  7077  snnen2og  7126  1nen2  7128  pm54.43  7500  en2eleq  7511  en2other2  7512  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  prarloclemarch2  7750  prarloclemlt  7824  prarloclemn  7830  hash2  11202  bj-el2oss1o  16672  pwle2  16898  nnsf  16909