Definition df-2o 6626

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 6619	. 2 class 2o
2		c1o 6618	. . 3 class 1o
3	2	csuc 4468	. 2 class suc 1o
4	1, 3	wceq 1398	1 wff 2o = suc 1o

This definition is referenced by:  2on  6634  2on0  6635  df2o3  6640  o1p1e2  6679  2onn  6732  nnm2  6737  enpr2d  7040  snnen2og  7088  1nen2  7090  pm54.43  7438  en2eleq  7449  en2other2  7450  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  prarloclemarch2  7682  prarloclemlt  7756  prarloclemn  7762  hash2  11122  bj-el2oss1o  16475  pwle2  16703  nnsf  16714