Definition df-2o 6002

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 5995	. 2 class 2𝑜
2		c1o 5994	. . 3 class 1𝑜
3	2	csuc 4102	. 2 class suc 1𝑜
4	1, 3	wceq 1243	1 wff 2𝑜 = suc 1𝑜

This definition is referenced by:  2on  6009  2on0  6010  df2o3  6014  o1p1e2  6048  2onn  6094  nnm2  6098  snnen2og  6322  prarloclemarch2  6517  prarloclemlt  6591  prarloclemn  6597