Definition df-7 12410

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 12402	. 2 class 7
2		c6 12401	. . 3 class 6
3		c1 11201	. . 3 class 1
4		caddc 11203	. . 3 class +
5	2, 3, 4	co 7420	. 2 class (6 + 1)
6	1, 5	wceq 1569	1 wff 7 = (6 + 1)

This definition is used by:  7nn  12435  7re  12436  7cn  12437  7m1e6  12474  6p1e7  12490  4p3e7  12496  5p2e7  12498  6p2e8  12501  6lt7  12531  7p7e14  12898  8p7e15  12904  9p7e16  12911  9p8e17  12912  7t7e49  12933  8t7e56  12939  9t7e63  12946  2exp7  17265  7prm  17288  17prm  17295  37prm  17299  317prm  17304  log2ublem2  27275  log2ublem3  27276  bclbnd  27607  bposlem8  27618  lgsdir2lem3  27654  problem4  36433  1p7e8  43315  3cubeslem3r  43698  rmydioph  44021  expdiophlem2  44029  fmtno5  48642  257prm  48646  127prm  48684  7odd  48810  stgoldbwt  48874