Definition df-5 9069

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 9061	. 2 class 5
2		c4 9060	. . 3 class 4
3		c1 7897	. . 3 class 1
4		caddc 7899	. . 3 class +
5	2, 3, 4	co 5925	. 2 class (4 + 1)
6	1, 5	wceq 1364	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  9086  5pos  9107  5m1e4  9129  4p1e5  9144  3p2e5  9149  4p2e6  9151  5nn  9172  4lt5  9183  5p5e10  9544  6p5e11  9546  7p5e12  9550  8p5e13  9556  8p7e15  9558  9p5e14  9563  9p6e15  9564  5t5e25  9576  6t5e30  9580  7t5e35  9585  8t5e40  9591  9t5e45  9598  fldiv4p1lem1div2  10412  ef01bndlem  11938  prm23lt5  12457  lgsdir2lem3  15355  2lgslem3c  15420  2lgsoddprmlem3c  15434  ex-exp  15457  ex-fac  15458  ex-bc  15459