Definition df-7 8981

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 8973	. 2 class 7
2		c6 8972	. . 3 class 6
3		c1 7811	. . 3 class 1
4		caddc 7813	. . 3 class +
5	2, 3, 4	co 5874	. 2 class (6 + 1)
6	1, 5	wceq 1353	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  9000  7pos  9019  7m1e6  9041  6p1e7  9055  4p3e7  9061  5p2e7  9063  6p2e8  9066  7nn  9083  6lt7  9101  7p7e14  9460  8p7e15  9466  9p7e16  9473  9p8e17  9474  7t7e49  9495  8t7e56  9501  9t7e63  9508  lgsdir2lem3  14324