Definition df-7 12246

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 12238	. 2 class 7
2		c6 12237	. . 3 class 6
3		c1 11036	. . 3 class 1
4		caddc 11038	. . 3 class +
5	2, 3, 4	co 7364	. 2 class (6 + 1)
6	1, 5	wceq 1542	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12270  7re  12271  7cn  12272  7pos  12289  7m1e6  12305  6p1e7  12321  4p3e7  12327  5p2e7  12329  6p2e8  12332  6lt7  12359  7p7e14  12720  8p7e15  12726  9p7e16  12733  9p8e17  12734  7t7e49  12755  8t7e56  12761  9t7e63  12768  2exp7  17055  7prm  17078  17prm  17084  37prm  17088  317prm  17093  log2ublem2  26908  log2ublem3  26909  bclbnd  27240  bposlem8  27251  lgsdir2lem3  27287  problem4  35847  3cubeslem3r  43116  rmydioph  43439  expdiophlem2  43447  fmtno5  48011  257prm  48015  127prm  48053  7odd  48179  stgoldbwt  48243