Definition df-7 12227

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 12219	. 2 class 7
2		c6 12218	. . 3 class 6
3		c1 11041	. . 3 class 1
4		caddc 11043	. . 3 class +
5	2, 3, 4	co 7370	. 2 class (6 + 1)
6	1, 5	wceq 1542	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12251  7re  12252  7cn  12253  7pos  12270  7m1e6  12286  6p1e7  12302  4p3e7  12308  5p2e7  12310  6p2e8  12313  6lt7  12340  7p7e14  12700  8p7e15  12706  9p7e16  12713  9p8e17  12714  7t7e49  12735  8t7e56  12741  9t7e63  12748  2exp7  17029  7prm  17052  17prm  17058  37prm  17062  317prm  17067  log2ublem2  26930  log2ublem3  26931  bclbnd  27264  bposlem8  27275  lgsdir2lem3  27311  problem4  35890  3cubeslem3r  43073  rmydioph  43400  expdiophlem2  43408  fmtno5  47946  257prm  47950  127prm  47988  7odd  48101  stgoldbwt  48165