Definition df-2o 6561

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 6554	. 2 class 2o
2		c1o 6553	. . 3 class 1o
3	2	csuc 4455	. 2 class suc 1o
4	1, 3	wceq 1395	1 wff 2o = suc 1o

This definition is referenced by:  2on  6569  2on0  6570  df2o3  6574  o1p1e2  6612  2onn  6665  nnm2  6670  enpr2d  6970  snnen2og  7016  1nen2  7018  pm54.43  7359  en2eleq  7369  en2other2  7370  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  prarloclemarch2  7602  prarloclemlt  7676  prarloclemn  7682  hash2  11029  bj-el2oss1o  16096  pwle2  16323  nnsf  16330