Definition df-7 12307

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 12299	. 2 class 7
2		c6 12298	. . 3 class 6
3		c1 11100	. . 3 class 1
4		caddc 11102	. . 3 class +
5	2, 3, 4	co 7410	. 2 class (6 + 1)
6	1, 5	wceq 1568	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12332  7re  12333  7cn  12334  7m1e6  12371  6p1e7  12387  4p3e7  12393  5p2e7  12395  6p2e8  12398  6lt7  12428  7p7e14  12794  8p7e15  12800  9p7e16  12807  9p8e17  12808  7t7e49  12829  8t7e56  12835  9t7e63  12842  2exp7  17146  7prm  17169  17prm  17176  37prm  17180  317prm  17185  log2ublem2  27088  log2ublem3  27089  bclbnd  27420  bposlem8  27431  lgsdir2lem3  27467  problem4  36114  3cubeslem3r  43366  rmydioph  43689  expdiophlem2  43697  fmtno5  48254  257prm  48258  127prm  48296  7odd  48422  stgoldbwt  48486