Definition df-7 12308

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 12300	. 2 class 7
2		c6 12299	. . 3 class 6
3		c1 11101	. . 3 class 1
4		caddc 11103	. . 3 class +
5	2, 3, 4	co 7411	. 2 class (6 + 1)
6	1, 5	wceq 1567	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12333  7re  12334  7cn  12335  7m1e6  12372  6p1e7  12388  4p3e7  12394  5p2e7  12396  6p2e8  12399  6lt7  12429  7p7e14  12795  8p7e15  12801  9p7e16  12808  9p8e17  12809  7t7e49  12830  8t7e56  12836  9t7e63  12843  2exp7  17147  7prm  17170  17prm  17177  37prm  17181  317prm  17186  log2ublem2  27078  log2ublem3  27079  bclbnd  27410  bposlem8  27421  lgsdir2lem3  27457  problem4  36093  3cubeslem3r  43344  rmydioph  43667  expdiophlem2  43675  fmtno5  48232  257prm  48236  127prm  48274  7odd  48400  stgoldbwt  48464