Definition df-7 12379

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 12371	. 2 class 7
2		c6 12370	. . 3 class 6
3		c1 11172	. . 3 class 1
4		caddc 11174	. . 3 class +
5	2, 3, 4	co 7408	. 2 class (6 + 1)
6	1, 5	wceq 1570	1 wff 7 = (6 + 1)

This definition is used by:  7nn  12404  7re  12405  7cn  12406  7m1e6  12443  6p1e7  12459  4p3e7  12465  5p2e7  12467  6p2e8  12470  6lt7  12500  7p7e14  12867  8p7e15  12873  9p7e16  12880  9p8e17  12881  7t7e49  12902  8t7e56  12908  9t7e63  12915  2exp7  17226  7prm  17249  17prm  17256  37prm  17260  317prm  17265  log2ublem2  27238  log2ublem3  27239  bclbnd  27570  bposlem8  27581  lgsdir2lem3  27617  problem4  36354  1p7e8  43234  3cubeslem3r  43636  rmydioph  43959  expdiophlem2  43967  fmtno5  48564  257prm  48568  127prm  48606  7odd  48732  stgoldbwt  48796