Definition df-7 12331

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 12323	. 2 class 7
2		c6 12322	. . 3 class 6
3		c1 11153	. . 3 class 1
4		caddc 11155	. . 3 class +
5	2, 3, 4	co 7430	. 2 class (6 + 1)
6	1, 5	wceq 1536	1 wff 7 = (6 + 1)

This definition is referenced by:  7nn  12355  7re  12356  7cn  12357  7pos  12374  7m1e6  12395  6p1e7  12411  4p3e7  12417  5p2e7  12419  6p2e8  12422  6lt7  12449  7p7e14  12809  8p7e15  12815  9p7e16  12822  9p8e17  12823  7t7e49  12844  8t7e56  12850  9t7e63  12857  2exp7  17121  7prm  17144  17prm  17150  37prm  17154  317prm  17159  log2ublem2  27004  log2ublem3  27005  bclbnd  27338  bposlem8  27349  lgsdir2lem3  27385  problem4  35652  3cubeslem3r  42674  rmydioph  43002  expdiophlem2  43010  fmtno5  47481  257prm  47485  127prm  47523  7odd  47636  stgoldbwt  47700