Definition df-7 12280

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 12272	. 2 class 7
2		c6 12271	. . 3 class 6
3		c1 11111	. . 3 class 1
4		caddc 11113	. . 3 class +
5	2, 3, 4	co 7409	. 2 class (6 + 1)
6	1, 5	wceq 1542	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12304  7re  12305  7cn  12306  7pos  12323  7m1e6  12344  6p1e7  12360  4p3e7  12366  5p2e7  12368  6p2e8  12371  6lt7  12398  7p7e14  12756  8p7e15  12762  9p7e16  12769  9p8e17  12770  7t7e49  12791  8t7e56  12797  9t7e63  12804  2exp7  17021  7prm  17044  17prm  17050  37prm  17054  317prm  17059  log2ublem2  26452  log2ublem3  26453  bclbnd  26783  bposlem8  26794  lgsdir2lem3  26830  problem4  34653  3cubeslem3r  41425  rmydioph  41753  expdiophlem2  41761  fmtno5  46225  257prm  46229  127prm  46267  7odd  46380  stgoldbwt  46444