Definition df-7 9082

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 9074	. 2 class 7
2		c6 9073	. . 3 class 6
3		c1 7908	. . 3 class 1
4		caddc 7910	. . 3 class +
5	2, 3, 4	co 5934	. 2 class (6 + 1)
6	1, 5	wceq 1372	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  9101  7pos  9120  7m1e6  9142  6p1e7  9157  4p3e7  9163  5p2e7  9165  6p2e8  9168  7nn  9185  6lt7  9203  7p7e14  9564  8p7e15  9570  9p7e16  9577  9p8e17  9578  7t7e49  9599  8t7e56  9605  9t7e63  9612  2exp7  12676  lgsdir2lem3  15425