Definition df-7 12335

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 12327	. 2 class 7
2		c6 12326	. . 3 class 6
3		c1 11128	. . 3 class 1
4		caddc 11130	. . 3 class +
5	2, 3, 4	co 7416	. 2 class (6 + 1)
6	1, 5	wceq 1570	1 wff 7 = (6 + 1)

This definition is used by:  7nn  12360  7re  12361  7cn  12362  7m1e6  12399  6p1e7  12415  4p3e7  12421  5p2e7  12423  6p2e8  12426  6lt7  12456  7p7e14  12823  8p7e15  12829  9p7e16  12836  9p8e17  12837  7t7e49  12858  8t7e56  12864  9t7e63  12871  2exp7  17183  7prm  17206  17prm  17213  37prm  17217  317prm  17222  log2ublem2  27182  log2ublem3  27183  bclbnd  27514  bposlem8  27525  lgsdir2lem3  27561  problem4  36234  1p7e8  43117  3cubeslem3r  43519  rmydioph  43842  expdiophlem2  43850  fmtno5  48447  257prm  48451  127prm  48489  7odd  48615  stgoldbwt  48679