Definition df-5 9183

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 9175	. 2 class 5
2		c4 9174	. . 3 class 4
3		c1 8011	. . 3 class 1
4		caddc 8013	. . 3 class +
5	2, 3, 4	co 6007	. 2 class (4 + 1)
6	1, 5	wceq 1395	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  9200  5pos  9221  5m1e4  9243  4p1e5  9258  3p2e5  9263  4p2e6  9265  5nn  9286  4lt5  9297  5p5e10  9659  6p5e11  9661  7p5e12  9665  8p5e13  9671  8p7e15  9673  9p5e14  9678  9p6e15  9679  5t5e25  9691  6t5e30  9695  7t5e35  9700  8t5e40  9706  9t5e45  9713  fldiv4p1lem1div2  10537  ef01bndlem  12282  prm23lt5  12801  lgsdir2lem3  15724  2lgslem3c  15789  2lgsoddprmlem3c  15803  ex-exp  16146  ex-fac  16147  ex-bc  16148