Definition df-2o 6025

Description: Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.)

Assertion

Ref	Expression
df-2o	⊢ 2𝑜 = suc 1𝑜

Detailed syntax breakdown of Definition df-2o

Step	Hyp	Ref	Expression
1		c2o 6018	. 2 class 2𝑜
2		c1o 6017	. . 3 class 1𝑜
3	2	csuc 4120	. 2 class suc 1𝑜
4	1, 3	wceq 1284	1 wff 2𝑜 = suc 1𝑜

This definition is referenced by:  2on  6032  2on0  6033  df2o3  6037  o1p1e2  6071  2onn  6117  nnm2  6121  snnen2og  6345  1nen2  6347  pm54.43  6459  prarloclemarch2  6609  prarloclemlt  6683  prarloclemn  6689