Definition df-7 11084

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 11075	. 2 class 7
2		c6 11074	. . 3 class 6
3		c1 9937	. . 3 class 1
4		caddc 9939	. . 3 class +
5	2, 3, 4	co 6650	. 2 class (6 + 1)
6	1, 5	wceq 1483	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  11103  7pos  11120  7m1e6  11141  6p1e7  11156  4p3e7  11163  5p2e7  11165  6p2e8  11169  7nn  11190  6lt7  11209  7p7e14  11609  8p7e15  11617  9p7e16  11625  9p8e17  11626  7t7e49  11653  8t7e56  11661  9t7e63  11668  7prm  15817  17prm  15824  37prm  15828  317prm  15833  log2ublem2  24674  log2ublem3  24675  bclbnd  25005  bposlem8  25016  lgsdir2lem3  25052  2lgslem3d  25124  problem4  31562  rmydioph  37581  expdiophlem2  37589  fmtno5  41469  257prm  41473  2exp7  41514  127prm  41515  7odd  41621  stgoldbwt  41664