Definition df-7 12254

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 12246	. 2 class 7
2		c6 12245	. . 3 class 6
3		c1 11069	. . 3 class 1
4		caddc 11071	. . 3 class +
5	2, 3, 4	co 7387	. 2 class (6 + 1)
6	1, 5	wceq 1540	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12278  7re  12279  7cn  12280  7pos  12297  7m1e6  12313  6p1e7  12329  4p3e7  12335  5p2e7  12337  6p2e8  12340  6lt7  12367  7p7e14  12728  8p7e15  12734  9p7e16  12741  9p8e17  12742  7t7e49  12763  8t7e56  12769  9t7e63  12776  2exp7  17058  7prm  17081  17prm  17087  37prm  17091  317prm  17096  log2ublem2  26857  log2ublem3  26858  bclbnd  27191  bposlem8  27202  lgsdir2lem3  27238  problem4  35655  3cubeslem3r  42675  rmydioph  43003  expdiophlem2  43011  fmtno5  47558  257prm  47562  127prm  47600  7odd  47713  stgoldbwt  47777