Definition df-2o 6578

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 6571	. 2 class 2o
2		c1o 6570	. . 3 class 1o
3	2	csuc 4460	. 2 class suc 1o
4	1, 3	wceq 1395	1 wff 2o = suc 1o

This definition is referenced by:  2on  6586  2on0  6587  df2o3  6592  o1p1e2  6631  2onn  6684  nnm2  6689  enpr2d  6992  snnen2og  7040  1nen2  7042  pm54.43  7386  en2eleq  7396  en2other2  7397  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  prarloclemarch2  7629  prarloclemlt  7703  prarloclemn  7709  hash2  11066  bj-el2oss1o  16306  pwle2  16535  nnsf  16543