Definition df-5 9204

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 9196	. 2 class 5
2		c4 9195	. . 3 class 4
3		c1 8032	. . 3 class 1
4		caddc 8034	. . 3 class +
5	2, 3, 4	co 6017	. 2 class (4 + 1)
6	1, 5	wceq 1397	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  9221  5pos  9242  5m1e4  9264  4p1e5  9279  3p2e5  9284  4p2e6  9286  5nn  9307  4lt5  9318  5p5e10  9680  6p5e11  9682  7p5e12  9686  8p5e13  9692  8p7e15  9694  9p5e14  9699  9p6e15  9700  5t5e25  9712  6t5e30  9716  7t5e35  9721  8t5e40  9727  9t5e45  9734  fldiv4p1lem1div2  10564  ef01bndlem  12316  prm23lt5  12835  lgsdir2lem3  15758  2lgslem3c  15823  2lgsoddprmlem3c  15837  ex-exp  16323  ex-fac  16324  ex-bc  16325