Definition df-7 12314

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 12306	. 2 class 7
2		c6 12305	. . 3 class 6
3		c1 11107	. . 3 class 1
4		caddc 11109	. . 3 class +
5	2, 3, 4	co 7412	. 2 class (6 + 1)
6	1, 5	wceq 1569	1 wff 7 = (6 + 1)

This definition is used by:  7nn  12339  7re  12340  7cn  12341  7m1e6  12378  6p1e7  12394  4p3e7  12400  5p2e7  12402  6p2e8  12405  6lt7  12435  7p7e14  12801  8p7e15  12807  9p7e16  12814  9p8e17  12815  7t7e49  12836  8t7e56  12842  9t7e63  12849  2exp7  17153  7prm  17176  17prm  17183  37prm  17187  317prm  17192  log2ublem2  27123  log2ublem3  27124  bclbnd  27455  bposlem8  27466  lgsdir2lem3  27502  problem4  36168  3cubeslem3r  43446  rmydioph  43769  expdiophlem2  43777  fmtno5  48337  257prm  48341  127prm  48379  7odd  48505  stgoldbwt  48569