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  7536  en2eleq  7547  en2other2  7548  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  prarloclemarch2  7786  prarloclemlt  7860  prarloclemn  7866  hash2  11253  bj-el2oss1o  16802  pwle2  17028  nnsf  17048