Definition df-7 12277

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 12269	. 2 class 7
2		c6 12268	. . 3 class 6
3		c1 11108	. . 3 class 1
4		caddc 11110	. . 3 class +
5	2, 3, 4	co 7406	. 2 class (6 + 1)
6	1, 5	wceq 1542	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12301  7re  12302  7cn  12303  7pos  12320  7m1e6  12341  6p1e7  12357  4p3e7  12363  5p2e7  12365  6p2e8  12368  6lt7  12395  7p7e14  12753  8p7e15  12759  9p7e16  12766  9p8e17  12767  7t7e49  12788  8t7e56  12794  9t7e63  12801  2exp7  17018  7prm  17041  17prm  17047  37prm  17051  317prm  17056  log2ublem2  26442  log2ublem3  26443  bclbnd  26773  bposlem8  26784  lgsdir2lem3  26820  problem4  34642  3cubeslem3r  41411  rmydioph  41739  expdiophlem2  41747  fmtno5  46212  257prm  46216  127prm  46254  7odd  46367  stgoldbwt  46431