Definition df-7 12217

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 12209	. 2 class 7
2		c6 12208	. . 3 class 6
3		c1 11031	. . 3 class 1
4		caddc 11033	. . 3 class +
5	2, 3, 4	co 7360	. 2 class (6 + 1)
6	1, 5	wceq 1542	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12241  7re  12242  7cn  12243  7pos  12260  7m1e6  12276  6p1e7  12292  4p3e7  12298  5p2e7  12300  6p2e8  12303  6lt7  12330  7p7e14  12690  8p7e15  12696  9p7e16  12703  9p8e17  12704  7t7e49  12725  8t7e56  12731  9t7e63  12738  2exp7  17019  7prm  17042  17prm  17048  37prm  17052  317prm  17057  log2ublem2  26917  log2ublem3  26918  bclbnd  27251  bposlem8  27262  lgsdir2lem3  27298  problem4  35864  3cubeslem3r  42996  rmydioph  43323  expdiophlem2  43331  fmtno5  47870  257prm  47874  127prm  47912  7odd  48025  stgoldbwt  48089