Definition df-7 12238

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 12230	. 2 class 7
2		c6 12229	. . 3 class 6
3		c1 11028	. . 3 class 1
4		caddc 11030	. . 3 class +
5	2, 3, 4	co 7356	. 2 class (6 + 1)
6	1, 5	wceq 1542	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12262  7re  12263  7cn  12264  7pos  12281  7m1e6  12297  6p1e7  12313  4p3e7  12319  5p2e7  12321  6p2e8  12324  6lt7  12351  7p7e14  12712  8p7e15  12718  9p7e16  12725  9p8e17  12726  7t7e49  12747  8t7e56  12753  9t7e63  12760  2exp7  17047  7prm  17070  17prm  17076  37prm  17080  317prm  17085  log2ublem2  26899  log2ublem3  26900  bclbnd  27231  bposlem8  27242  lgsdir2lem3  27278  problem4  35838  3cubeslem3r  43107  rmydioph  43430  expdiophlem2  43438  fmtno5  48008  257prm  48012  127prm  48050  7odd  48176  stgoldbwt  48240