Definition df-5 9054

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 9046	. 2 class 5
2		c4 9045	. . 3 class 4
3		c1 7882	. . 3 class 1
4		caddc 7884	. . 3 class +
5	2, 3, 4	co 5923	. 2 class (4 + 1)
6	1, 5	wceq 1364	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  9071  5pos  9092  5m1e4  9114  4p1e5  9129  3p2e5  9134  4p2e6  9136  5nn  9157  4lt5  9168  5p5e10  9529  6p5e11  9531  7p5e12  9535  8p5e13  9541  8p7e15  9543  9p5e14  9548  9p6e15  9549  5t5e25  9561  6t5e30  9565  7t5e35  9570  8t5e40  9576  9t5e45  9583  fldiv4p1lem1div2  10397  ef01bndlem  11923  prm23lt5  12442  lgsdir2lem3  15281  2lgslem3c  15346  2lgsoddprmlem3c  15360  ex-exp  15383  ex-fac  15384  ex-bc  15385