Definition df-2o 6569

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 6562	. 2 class 2o
2		c1o 6561	. . 3 class 1o
3	2	csuc 4456	. 2 class suc 1o
4	1, 3	wceq 1395	1 wff 2o = suc 1o

This definition is referenced by:  2on  6577  2on0  6578  df2o3  6583  o1p1e2  6622  2onn  6675  nnm2  6680  enpr2d  6980  snnen2og  7028  1nen2  7030  pm54.43  7374  en2eleq  7384  en2other2  7385  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  prarloclemarch2  7617  prarloclemlt  7691  prarloclemn  7697  hash2  11047  bj-el2oss1o  16193  pwle2  16423  nnsf  16431