Definition df-7 9135

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 9127	. 2 class 7
2		c6 9126	. . 3 class 6
3		c1 7961	. . 3 class 1
4		caddc 7963	. . 3 class +
5	2, 3, 4	co 5967	. 2 class ( 6 + 1 )
6	1, 5	wceq 1373	1 wff 7 = ( 6 + 1 )

This definition is referenced by:  7re  9154  7pos  9173  7m1e6  9195  6p1e7  9210  4p3e7  9216  5p2e7  9218  6p2e8  9221  7nn  9238  6lt7  9256  7p7e14  9617  8p7e15  9623  9p7e16  9630  9p8e17  9631  7t7e49  9652  8t7e56  9658  9t7e63  9665  2exp7  12872  lgsdir2lem3  15622