Definition df-5 9071

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 9063	. 2 class 5
2		c4 9062	. . 3 class 4
3		c1 7899	. . 3 class 1
4		caddc 7901	. . 3 class +
5	2, 3, 4	co 5925	. 2 class (4 + 1)
6	1, 5	wceq 1364	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  9088  5pos  9109  5m1e4  9131  4p1e5  9146  3p2e5  9151  4p2e6  9153  5nn  9174  4lt5  9185  5p5e10  9546  6p5e11  9548  7p5e12  9552  8p5e13  9558  8p7e15  9560  9p5e14  9565  9p6e15  9566  5t5e25  9578  6t5e30  9582  7t5e35  9587  8t5e40  9593  9t5e45  9600  fldiv4p1lem1div2  10414  ef01bndlem  11940  prm23lt5  12459  lgsdir2lem3  15379  2lgslem3c  15444  2lgsoddprmlem3c  15458  ex-exp  15481  ex-fac  15482  ex-bc  15483