Definition df-7 9100

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 9092	. 2 class 7
2		c6 9091	. . 3 class 6
3		c1 7926	. . 3 class 1
4		caddc 7928	. . 3 class +
5	2, 3, 4	co 5944	. 2 class ( 6 + 1 )
6	1, 5	wceq 1373	1 wff 7 = ( 6 + 1 )

This definition is referenced by:  7re  9119  7pos  9138  7m1e6  9160  6p1e7  9175  4p3e7  9181  5p2e7  9183  6p2e8  9186  7nn  9203  6lt7  9221  7p7e14  9582  8p7e15  9588  9p7e16  9595  9p8e17  9596  7t7e49  9617  8t7e56  9623  9t7e63  9630  2exp7  12757  lgsdir2lem3  15507