Definition df-7 9318

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 9310	. 2 class 7
2		c6 9309	. . 3 class 6
3		c1 8144	. . 3 class 1
4		caddc 8146	. . 3 class +
5	2, 3, 4	co 6058	. 2 class (6 + 1)
6	1, 5	wceq 1398	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  9337  7pos  9356  7m1e6  9378  6p1e7  9393  4p3e7  9399  5p2e7  9401  6p2e8  9404  7nn  9421  6lt7  9439  7p7e14  9805  8p7e15  9811  9p7e16  9818  9p8e17  9819  7t7e49  9840  8t7e56  9846  9t7e63  9853  2exp7  13157  lgsdir2lem3  16029