Definition df-7 8808

Description: Define the number 7. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
df-7	⊢ 7 = (6 + 1)

Detailed syntax breakdown of Definition df-7

Step	Hyp	Ref	Expression
1		c7 8800	. 2 class 7
2		c6 8799	. . 3 class 6
3		c1 7645	. . 3 class 1
4		caddc 7647	. . 3 class +
5	2, 3, 4	co 5782	. 2 class (6 + 1)
6	1, 5	wceq 1332	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  8827  7pos  8846  7m1e6  8868  6p1e7  8882  4p3e7  8888  5p2e7  8890  6p2e8  8893  7nn  8910  6lt7  8928  7p7e14  9284  8p7e15  9290  9p7e16  9297  9p8e17  9298  7t7e49  9319  8t7e56  9325  9t7e63  9332