Definition df-5 9098

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 9090	. 2 class 5
2		c4 9089	. . 3 class 4
3		c1 7926	. . 3 class 1
4		caddc 7928	. . 3 class +
5	2, 3, 4	co 5944	. 2 class ( 4 + 1 )
6	1, 5	wceq 1373	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  9115  5pos  9136  5m1e4  9158  4p1e5  9173  3p2e5  9178  4p2e6  9180  5nn  9201  4lt5  9212  5p5e10  9574  6p5e11  9576  7p5e12  9580  8p5e13  9586  8p7e15  9588  9p5e14  9593  9p6e15  9594  5t5e25  9606  6t5e30  9610  7t5e35  9615  8t5e40  9621  9t5e45  9628  fldiv4p1lem1div2  10448  ef01bndlem  12067  prm23lt5  12586  lgsdir2lem3  15507  2lgslem3c  15572  2lgsoddprmlem3c  15586  ex-exp  15663  ex-fac  15664  ex-bc  15665