Definition df-5 9097

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 9089	. 2 class 5
2		c4 9088	. . 3 class 4
3		c1 7925	. . 3 class 1
4		caddc 7927	. . 3 class +
5	2, 3, 4	co 5943	. 2 class (4 + 1)
6	1, 5	wceq 1372	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  9114  5pos  9135  5m1e4  9157  4p1e5  9172  3p2e5  9177  4p2e6  9179  5nn  9200  4lt5  9211  5p5e10  9573  6p5e11  9575  7p5e12  9579  8p5e13  9585  8p7e15  9587  9p5e14  9592  9p6e15  9593  5t5e25  9605  6t5e30  9609  7t5e35  9614  8t5e40  9620  9t5e45  9627  fldiv4p1lem1div2  10446  ef01bndlem  12009  prm23lt5  12528  lgsdir2lem3  15449  2lgslem3c  15514  2lgsoddprmlem3c  15528  ex-exp  15596  ex-fac  15597  ex-bc  15598