Definition df-5 9248

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 9240	. 2 class 5
2		c4 9239	. . 3 class 4
3		c1 8076	. . 3 class 1
4		caddc 8078	. . 3 class +
5	2, 3, 4	co 6028	. 2 class (4 + 1)
6	1, 5	wceq 1398	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  9265  5pos  9286  5m1e4  9308  4p1e5  9323  3p2e5  9328  4p2e6  9330  5nn  9351  4lt5  9362  5p5e10  9724  6p5e11  9726  7p5e12  9730  8p5e13  9736  8p7e15  9738  9p5e14  9743  9p6e15  9744  5t5e25  9756  6t5e30  9760  7t5e35  9765  8t5e40  9771  9t5e45  9778  fldiv4p1lem1div2  10609  ef01bndlem  12378  prm23lt5  12897  lgsdir2lem3  15829  2lgslem3c  15894  2lgsoddprmlem3c  15908  ex-exp  16421  ex-fac  16422  ex-bc  16423