Metamath Proof Explorer


Definition df-2

Description: Define the number 2. (Contributed by NM, 27-May-1999)

Ref Expression
Assertion df-2 2=1+1

Detailed syntax breakdown

Step Hyp Ref Expression
0 c2 class2
1 c1 class1
2 caddc class+
3 1 1 2 co class1+1
4 0 3 wceq wff2=1+1