Definition df-7 8985

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 8977	. 2 class 7
2		c6 8976	. . 3 class 6
3		c1 7814	. . 3 class 1
4		caddc 7816	. . 3 class +
5	2, 3, 4	co 5877	. 2 class (6 + 1)
6	1, 5	wceq 1353	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  9004  7pos  9023  7m1e6  9045  6p1e7  9059  4p3e7  9065  5p2e7  9067  6p2e8  9070  7nn  9087  6lt7  9105  7p7e14  9464  8p7e15  9470  9p7e16  9477  9p8e17  9478  7t7e49  9499  8t7e56  9505  9t7e63  9512  lgsdir2lem3  14470