Definition df-7 9377

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 9369	. 2 class 7
2		c6 9368	. . 3 class 6
3		c1 8186	. . 3 class 1
4		caddc 8188	. . 3 class +
5	2, 3, 4	co 6088	. 2 class ( 6 + 1 )
6	1, 5	wceq 1402	1 wff 7 = ( 6 + 1 )

This definition is used by:  7re  9396  7pos  9415  7m1e6  9437  6p1e7  9452  4p3e7  9458  5p2e7  9460  6p2e8  9463  7nn  9482  6lt7  9500  7p7e14  9870  8p7e15  9876  9p7e16  9883  9p8e17  9884  7t7e49  9905  8t7e56  9911  9t7e63  9918  2exp7  13242  7prm  13253  17prm  13259  37prm  13263  317prm  13268  log2ublem2  16239  log2ublem3  16240  bclbnd  16324  bposlem8  16335  lgsdir2lem3  16371