Definition df-5 9316

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 9308	. 2 class 5
2		c4 9307	. . 3 class 4
3		c1 8144	. . 3 class 1
4		caddc 8146	. . 3 class +
5	2, 3, 4	co 6058	. 2 class (4 + 1)
6	1, 5	wceq 1398	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  9333  5pos  9354  5m1e4  9376  4p1e5  9391  3p2e5  9396  4p2e6  9398  5nn  9419  4lt5  9430  5p5e10  9797  6p5e11  9799  7p5e12  9803  8p5e13  9809  8p7e15  9811  9p5e14  9816  9p6e15  9817  5t5e25  9829  6t5e30  9833  7t5e35  9838  8t5e40  9844  9t5e45  9851  fldiv4p1lem1div2  10689  ef01bndlem  12467  prm23lt5  12986  lgsdir2lem3  16029  2lgslem3c  16094  2lgsoddprmlem3c  16108  ex-exp  16621  ex-fac  16622  ex-bc  16623