Definition df-7 9054

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 9046	. 2 class 7
2		c6 9045	. . 3 class 6
3		c1 7880	. . 3 class 1
4		caddc 7882	. . 3 class +
5	2, 3, 4	co 5922	. 2 class (6 + 1)
6	1, 5	wceq 1364	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  9073  7pos  9092  7m1e6  9114  6p1e7  9129  4p3e7  9135  5p2e7  9137  6p2e8  9140  7nn  9157  6lt7  9175  7p7e14  9535  8p7e15  9541  9p7e16  9548  9p8e17  9549  7t7e49  9570  8t7e56  9576  9t7e63  9583  2exp7  12603  lgsdir2lem3  15271