Definition df-5 8980

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

Assertion

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

Detailed syntax breakdown of Definition df-5

Step	Hyp	Ref	Expression
1		c5 8972	. 2 class 5
2		c4 8971	. . 3 class 4
3		c1 7811	. . 3 class 1
4		caddc 7813	. . 3 class +
5	2, 3, 4	co 5874	. 2 class (4 + 1)
6	1, 5	wceq 1353	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  8997  5pos  9018  5m1e4  9040  4p1e5  9054  3p2e5  9059  4p2e6  9061  5nn  9082  4lt5  9093  5p5e10  9453  6p5e11  9455  7p5e12  9459  8p5e13  9465  8p7e15  9467  9p5e14  9472  9p6e15  9473  5t5e25  9485  6t5e30  9489  7t5e35  9494  8t5e40  9500  9t5e45  9507  fldiv4p1lem1div2  10304  ef01bndlem  11763  prm23lt5  12262  lgsdir2lem3  14401  2lgsoddprmlem3c  14427  ex-exp  14449  ex-fac  14450  ex-bc  14451