Definition df-5 8915

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 8907	. 2 class 5
2		c4 8906	. . 3 class 4
3		c1 7750	. . 3 class 1
4		caddc 7752	. . 3 class +
5	2, 3, 4	co 5841	. 2 class (4 + 1)
6	1, 5	wceq 1343	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  8932  5pos  8953  5m1e4  8975  4p1e5  8989  3p2e5  8994  4p2e6  8996  5nn  9017  4lt5  9028  5p5e10  9388  6p5e11  9390  7p5e12  9394  8p5e13  9400  8p7e15  9402  9p5e14  9407  9p6e15  9408  5t5e25  9420  6t5e30  9424  7t5e35  9429  8t5e40  9435  9t5e45  9442  fldiv4p1lem1div2  10236  ef01bndlem  11693  prm23lt5  12191  lgsdir2lem3  13531  ex-exp  13568  ex-fac  13569  ex-bc  13570