Definition df-5 8782

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 8774	. 2 class 5
2		c4 8773	. . 3 class 4
3		c1 7621	. . 3 class 1
4		caddc 7623	. . 3 class +
5	2, 3, 4	co 5774	. 2 class ( 4 + 1 )
6	1, 5	wceq 1331	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  8799  5pos  8820  5m1e4  8842  4p1e5  8856  3p2e5  8861  4p2e6  8863  5nn  8884  4lt5  8895  5p5e10  9252  6p5e11  9254  7p5e12  9258  8p5e13  9264  8p7e15  9266  9p5e14  9271  9p6e15  9272  5t5e25  9284  6t5e30  9288  7t5e35  9293  8t5e40  9299  9t5e45  9306  fldiv4p1lem1div2  10078  ef01bndlem  11463  ex-exp  12939  ex-fac  12940  ex-bc  12941