Definition df-2o 6526

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 6519	. 2 class 2o
2		c1o 6518	. . 3 class 1o
3	2	csuc 4430	. 2 class suc 1o
4	1, 3	wceq 1373	1 wff 2o = suc 1o

This definition is referenced by:  2on  6534  2on0  6535  df2o3  6539  o1p1e2  6577  2onn  6630  nnm2  6635  enpr2d  6935  snnen2og  6981  1nen2  6983  pm54.43  7324  en2eleq  7334  en2other2  7335  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  prarloclemarch2  7567  prarloclemlt  7641  prarloclemn  7647  hash2  10994  bj-el2oss1o  15910  pwle2  16137  nnsf  16144