Definition df-2o 6420

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 6413	. 2 class 2o
2		c1o 6412	. . 3 class 1o
3	2	csuc 4367	. 2 class suc 1o
4	1, 3	wceq 1353	1 wff 2o = suc 1o

This definition is referenced by:  2on  6428  2on0  6429  df2o3  6433  o1p1e2  6471  2onn  6524  nnm2  6529  enpr2d  6819  snnen2og  6861  1nen2  6863  pm54.43  7191  en2eleq  7196  en2other2  7197  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  prarloclemarch2  7420  prarloclemlt  7494  prarloclemn  7500  hash2  10794  bj-el2oss1o  14565  pwle2  14787  nnsf  14793