Definition df-7 9170

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 9162	. 2 class 7
2		c6 9161	. . 3 class 6
3		c1 7996	. . 3 class 1
4		caddc 7998	. . 3 class +
5	2, 3, 4	co 6000	. 2 class (6 + 1)
6	1, 5	wceq 1395	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  9189  7pos  9208  7m1e6  9230  6p1e7  9245  4p3e7  9251  5p2e7  9253  6p2e8  9256  7nn  9273  6lt7  9291  7p7e14  9652  8p7e15  9658  9p7e16  9665  9p8e17  9666  7t7e49  9687  8t7e56  9693  9t7e63  9700  2exp7  12952  lgsdir2lem3  15703