Metamath Proof Explorer


Definition df-4

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

Ref Expression
Assertion df-4 4 = 3 + 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 c4 class 4
1 c3 class 3
2 caddc class +
3 c1 class 1
4 1 3 2 co class 3 + 1
5 0 4 wceq wff 4 = 3 + 1