Definition df-5 9052

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 9044	. 2 class 5
2		c4 9043	. . 3 class 4
3		c1 7880	. . 3 class 1
4		caddc 7882	. . 3 class +
5	2, 3, 4	co 5922	. 2 class (4 + 1)
6	1, 5	wceq 1364	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  9069  5pos  9090  5m1e4  9112  4p1e5  9127  3p2e5  9132  4p2e6  9134  5nn  9155  4lt5  9166  5p5e10  9527  6p5e11  9529  7p5e12  9533  8p5e13  9539  8p7e15  9541  9p5e14  9546  9p6e15  9547  5t5e25  9559  6t5e30  9563  7t5e35  9568  8t5e40  9574  9t5e45  9581  fldiv4p1lem1div2  10395  ef01bndlem  11921  prm23lt5  12432  lgsdir2lem3  15271  2lgslem3c  15336  2lgsoddprmlem3c  15350  ex-exp  15373  ex-fac  15374  ex-bc  15375