Definition df-7 12050

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 12042	. 2 class 7
2		c6 12041	. . 3 class 6
3		c1 10881	. . 3 class 1
4		caddc 10883	. . 3 class +
5	2, 3, 4	co 7284	. 2 class (6 + 1)
6	1, 5	wceq 1539	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12074  7re  12075  7cn  12076  7pos  12093  7m1e6  12114  6p1e7  12130  4p3e7  12136  5p2e7  12138  6p2e8  12141  6lt7  12168  7p7e14  12525  8p7e15  12531  9p7e16  12538  9p8e17  12539  7t7e49  12560  8t7e56  12566  9t7e63  12573  2exp7  16798  7prm  16821  17prm  16827  37prm  16831  317prm  16836  log2ublem2  26106  log2ublem3  26107  bclbnd  26437  bposlem8  26448  lgsdir2lem3  26484  problem4  33635  3cubeslem3r  40516  rmydioph  40843  expdiophlem2  40851  fmtno5  45020  257prm  45024  127prm  45062  7odd  45175  stgoldbwt  45239