Definition df-7 9197

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 9189	. 2 class 7
2		c6 9188	. . 3 class 6
3		c1 8023	. . 3 class 1
4		caddc 8025	. . 3 class +
5	2, 3, 4	co 6013	. 2 class (6 + 1)
6	1, 5	wceq 1395	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  9216  7pos  9235  7m1e6  9257  6p1e7  9272  4p3e7  9278  5p2e7  9280  6p2e8  9283  7nn  9300  6lt7  9318  7p7e14  9679  8p7e15  9685  9p7e16  9692  9p8e17  9693  7t7e49  9714  8t7e56  9720  9t7e63  9727  2exp7  12997  lgsdir2lem3  15749