Definition df-6 8783

Description: Define the number 6. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
df-6	⊢ 6 = (5 + 1)

Detailed syntax breakdown of Definition df-6

Step	Hyp	Ref	Expression
1		c6 8775	. 2 class 6
2		c5 8774	. . 3 class 5
3		c1 7621	. . 3 class 1
4		caddc 7623	. . 3 class +
5	2, 3, 4	co 5774	. 2 class (5 + 1)
6	1, 5	wceq 1331	1 wff 6 = (5 + 1)

This definition is referenced by:  6re  8801  6pos  8821  6m1e5  8843  5p1e6  8857  3p3e6  8862  4p2e6  8863  5p2e7  8866  6nn  8885  5lt6  8899  6p6e12  9255  7p6e13  9259  8p6e14  9265  8p8e16  9267  9p6e15  9272  9p7e16  9273  6t6e36  9289  7t6e42  9294  8t6e48  9300  9t6e54  9307