Definition df-5 9118

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 9110	. 2 class 5
2		c4 9109	. . 3 class 4
3		c1 7946	. . 3 class 1
4		caddc 7948	. . 3 class +
5	2, 3, 4	co 5957	. 2 class (4 + 1)
6	1, 5	wceq 1373	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  9135  5pos  9156  5m1e4  9178  4p1e5  9193  3p2e5  9198  4p2e6  9200  5nn  9221  4lt5  9232  5p5e10  9594  6p5e11  9596  7p5e12  9600  8p5e13  9606  8p7e15  9608  9p5e14  9613  9p6e15  9614  5t5e25  9626  6t5e30  9630  7t5e35  9635  8t5e40  9641  9t5e45  9648  fldiv4p1lem1div2  10470  ef01bndlem  12142  prm23lt5  12661  lgsdir2lem3  15582  2lgslem3c  15647  2lgsoddprmlem3c  15661  ex-exp  15802  ex-fac  15803  ex-bc  15804