Metamath Proof Explorer


Definition df-2o

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 c2o class 2 𝑜
1 c1o class 1 𝑜
2 1 csuc class suc 1 𝑜
3 0 2 wceq wff 2 𝑜 = suc 1 𝑜