Definition df-2o 6502

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 6495	. 2 class 2o
2		c1o 6494	. . 3 class 1o
3	2	csuc 4411	. 2 class suc 1o
4	1, 3	wceq 1372	1 wff 2o = suc 1o

This definition is referenced by:  2on  6510  2on0  6511  df2o3  6515  o1p1e2  6553  2onn  6606  nnm2  6611  enpr2d  6910  snnen2og  6955  1nen2  6957  pm54.43  7297  en2eleq  7302  en2other2  7303  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  prarloclemarch2  7531  prarloclemlt  7605  prarloclemn  7611  hash2  10955  bj-el2oss1o  15643  pwle2  15868  nnsf  15875