Definition df-7 12306

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 12298	. 2 class 7
2		c6 12297	. . 3 class 6
3		c1 11128	. . 3 class 1
4		caddc 11130	. . 3 class +
5	2, 3, 4	co 7403	. 2 class (6 + 1)
6	1, 5	wceq 1540	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12330  7re  12331  7cn  12332  7pos  12349  7m1e6  12370  6p1e7  12386  4p3e7  12392  5p2e7  12394  6p2e8  12397  6lt7  12424  7p7e14  12785  8p7e15  12791  9p7e16  12798  9p8e17  12799  7t7e49  12820  8t7e56  12826  9t7e63  12833  2exp7  17105  7prm  17128  17prm  17134  37prm  17138  317prm  17143  log2ublem2  26907  log2ublem3  26908  bclbnd  27241  bposlem8  27252  lgsdir2lem3  27288  problem4  35636  3cubeslem3r  42657  rmydioph  42985  expdiophlem2  42993  fmtno5  47519  257prm  47523  127prm  47561  7odd  47674  stgoldbwt  47738