Definition df-2o 6688

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 6681	. 2 class 2o
2		c1o 6680	. . 3 class 1o
3	2	csuc 4510	. 2 class suc 1o
4	1, 3	wceq 1402	1 wff 2o = suc 1o

This definition is used by:  2on  6696  2on0  6697  df2o3  6702  o1p1e2  6741  2onn  6794  nnm2  6799  enpr2d  7111  snnen2og  7160  1nen2  7162  pm54.43  7537  en2eleq  7548  en2other2  7549  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  prarloclemarch2  7787  prarloclemlt  7861  prarloclemn  7867  hash2  11269  bj-el2oss1o  16968  pwle2  17194  nnsf  17214