Definition df-7 12199

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 12191	. 2 class 7
2		c6 12190	. . 3 class 6
3		c1 11013	. . 3 class 1
4		caddc 11015	. . 3 class +
5	2, 3, 4	co 7352	. 2 class (6 + 1)
6	1, 5	wceq 1541	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12223  7re  12224  7cn  12225  7pos  12242  7m1e6  12258  6p1e7  12274  4p3e7  12280  5p2e7  12282  6p2e8  12285  6lt7  12312  7p7e14  12673  8p7e15  12679  9p7e16  12686  9p8e17  12687  7t7e49  12708  8t7e56  12714  9t7e63  12721  2exp7  17005  7prm  17028  17prm  17034  37prm  17038  317prm  17043  log2ublem2  26890  log2ublem3  26891  bclbnd  27224  bposlem8  27235  lgsdir2lem3  27271  problem4  35719  3cubeslem3r  42785  rmydioph  43112  expdiophlem2  43120  fmtno5  47662  257prm  47666  127prm  47704  7odd  47817  stgoldbwt  47881