Definition df-7 12261

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 12253	. 2 class 7
2		c6 12252	. . 3 class 6
3		c1 11076	. . 3 class 1
4		caddc 11078	. . 3 class +
5	2, 3, 4	co 7390	. 2 class (6 + 1)
6	1, 5	wceq 1540	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12285  7re  12286  7cn  12287  7pos  12304  7m1e6  12320  6p1e7  12336  4p3e7  12342  5p2e7  12344  6p2e8  12347  6lt7  12374  7p7e14  12735  8p7e15  12741  9p7e16  12748  9p8e17  12749  7t7e49  12770  8t7e56  12776  9t7e63  12783  2exp7  17065  7prm  17088  17prm  17094  37prm  17098  317prm  17103  log2ublem2  26864  log2ublem3  26865  bclbnd  27198  bposlem8  27209  lgsdir2lem3  27245  problem4  35662  3cubeslem3r  42682  rmydioph  43010  expdiophlem2  43018  fmtno5  47562  257prm  47566  127prm  47604  7odd  47717  stgoldbwt  47781