Definition df-5 8101

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 8092	. 2 class 5
2		c4 8091	. . 3 class 4
3		c1 6982	. . 3 class 1
4		caddc 6984	. . 3 class +
5	2, 3, 4	co 5532	. 2 class (4 + 1)
6	1, 5	wceq 1284	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  8118  5pos  8139  4p1e5  8168  3p2e5  8173  4p2e6  8175  5nn  8196  4lt5  8207  5p5e10  8547  6p5e11  8549  7p5e12  8553  8p5e13  8559  8p7e15  8561  9p5e14  8566  9p6e15  8567  5t5e25  8579  6t5e30  8583  7t5e35  8588  8t5e40  8594  9t5e45  8601  fldiv4p1lem1div2  9307  ex-fac  10565  ex-bc  10566