Definition df-5 8806

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 8798	. 2 class 5
2		c4 8797	. . 3 class 4
3		c1 7645	. . 3 class 1
4		caddc 7647	. . 3 class +
5	2, 3, 4	co 5782	. 2 class (4 + 1)
6	1, 5	wceq 1332	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  8823  5pos  8844  5m1e4  8866  4p1e5  8880  3p2e5  8885  4p2e6  8887  5nn  8908  4lt5  8919  5p5e10  9276  6p5e11  9278  7p5e12  9282  8p5e13  9288  8p7e15  9290  9p5e14  9295  9p6e15  9296  5t5e25  9308  6t5e30  9312  7t5e35  9317  8t5e40  9323  9t5e45  9330  fldiv4p1lem1div2  10109  ef01bndlem  11499  ex-exp  13110  ex-fac  13111  ex-bc  13112