Definition df-7 12434

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 12426	. 2 class 7
2		c6 12425	. . 3 class 6
3		c1 11225	. . 3 class 1
4		caddc 11227	. . 3 class +
5	2, 3, 4	co 7440	. 2 class (6 + 1)
6	1, 5	wceq 1570	1 wff 7 = (6 + 1)

This definition is used by:  7nn  12459  7re  12460  7cn  12461  7m1e6  12498  6p1e7  12514  4p3e7  12520  5p2e7  12522  6p2e8  12525  6lt7  12555  7p7e14  12922  8p7e15  12928  9p7e16  12935  9p8e17  12936  7t7e49  12957  8t7e56  12963  9t7e63  12970  2exp7  17291  7prm  17314  17prm  17321  37prm  17325  317prm  17330  log2ublem2  27302  log2ublem3  27303  bclbnd  27634  bposlem8  27645  lgsdir2lem3  27681  problem4  36599  1p7e8  43505  3cubeslem3r  43888  rmydioph  44212  expdiophlem2  44220  fmtno5  48845  257prm  48849  127prm  48887  7odd  49013  stgoldbwt  49077