Definition df-5 7974

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

Assertion

Ref	Expression
df-5	⊢ 5 = (4 + 1)

Detailed syntax breakdown of Definition df-5

Step	Hyp	Ref	Expression
1		c5 7965	. 2 class 5
2		c4 7964	. . 3 class 4
3		c1 6888	. . 3 class 1
4		caddc 6890	. . 3 class +
5	2, 3, 4	co 5512	. 2 class (4 + 1)
6	1, 5	wceq 1243	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  7992  5pos  8014  4p1e5  8044  3p2e5  8050  4p2e6  8052  5p5e10  8058  5nn  8078  4lt5  8090  6p5e11  8415  7p5e12  8418  8p5e13  8423  8p7e15  8425  9p5e14  8430  9p6e15  8431  5t5e25  8441  6t5e30  8445  7t5e35  8450  8t5e40  8456  9t5e45  8463  fldiv4p1lem1div2  9145