Definition df-7 9207

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 9199	. 2 class 7
2		c6 9198	. . 3 class 6
3		c1 8033	. . 3 class 1
4		caddc 8035	. . 3 class +
5	2, 3, 4	co 6018	. 2 class (6 + 1)
6	1, 5	wceq 1397	1 wff 7 = (6 + 1)

This definition is referenced by:  7re  9226  7pos  9245  7m1e6  9267  6p1e7  9282  4p3e7  9288  5p2e7  9290  6p2e8  9293  7nn  9310  6lt7  9328  7p7e14  9689  8p7e15  9695  9p7e16  9702  9p8e17  9703  7t7e49  9724  8t7e56  9730  9t7e63  9737  2exp7  13025  lgsdir2lem3  15778