Definition df-2o 5941

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 5934	. 2 class 2𝑜
2		c1o 5933	. . 3 class 1𝑜
3	2	csuc 4068	. 2 class suc 1𝑜
4	1, 3	wceq 1242	1 wff 2𝑜 = suc 1𝑜

This definition is referenced by:  2on  5948  2on0  5949  df2o3  5953  o1p1e2  5987  2onn  6030  nnm2  6034  prarloclemarch2  6402  prarloclemlt  6475  prarloclemn  6481