Definition df-7 11971

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 11963	. 2 class 7
2		c6 11962	. . 3 class 6
3		c1 10803	. . 3 class 1
4		caddc 10805	. . 3 class +
5	2, 3, 4	co 7255	. 2 class (6 + 1)
6	1, 5	wceq 1539	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  11995  7re  11996  7cn  11997  7pos  12014  7m1e6  12035  6p1e7  12051  4p3e7  12057  5p2e7  12059  6p2e8  12062  6lt7  12089  7p7e14  12445  8p7e15  12451  9p7e16  12458  9p8e17  12459  7t7e49  12480  8t7e56  12486  9t7e63  12493  2exp7  16717  7prm  16740  17prm  16746  37prm  16750  317prm  16755  log2ublem2  26002  log2ublem3  26003  bclbnd  26333  bposlem8  26344  lgsdir2lem3  26380  problem4  33526  3cubeslem3r  40425  rmydioph  40752  expdiophlem2  40760  fmtno5  44897  257prm  44901  127prm  44939  7odd  45052  stgoldbwt  45116