Definition df-5 8484

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 8476	. 2 class 5
2		c4 8475	. . 3 class 4
3		c1 7351	. . 3 class 1
4		caddc 7353	. . 3 class +
5	2, 3, 4	co 5652	. 2 class (4 + 1)
6	1, 5	wceq 1289	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  8501  5pos  8522  4p1e5  8552  3p2e5  8557  4p2e6  8559  5nn  8580  4lt5  8591  5p5e10  8947  6p5e11  8949  7p5e12  8953  8p5e13  8959  8p7e15  8961  9p5e14  8966  9p6e15  8967  5t5e25  8979  6t5e30  8983  7t5e35  8988  8t5e40  8994  9t5e45  9001  fldiv4p1lem1div2  9712  ef01bndlem  11047  ex-exp  11654  ex-fac  11655  ex-bc  11656