Definition df-5 11445

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 11437	. 2 class 5
2		c4 11436	. . 3 class 4
3		c1 10275	. . 3 class 1
4		caddc 10277	. . 3 class +
5	2, 3, 4	co 6924	. 2 class (4 + 1)
6	1, 5	wceq 1601	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  11467  5re  11468  5cn  11469  5pos  11495  5m1e4  11516  4p1e5  11532  3p2e5  11537  4p2e6  11539  4lt5  11563  5p5e10  11922  6p5e11  11924  7p5e12  11928  8p5e13  11934  8p7e15  11936  9p5e14  11941  9p6e15  11942  5t5e25  11954  6t5e30  11958  7t5e35  11963  8t5e40  11969  9t5e45  11976  fldiv4p1lem1div2  12959  ef01bndlem  15320  prm23lt5  15927  5prm  16218  lt6abl  18686  log2ublem3  25131  ppiublem2  25384  bclbnd  25461  bposlem6  25470  bposlem9  25473  lgsdir2lem3  25508  2lgslem3c  25579  2lgsoddprmlem3c  25593  ex-exp  27886  ex-fac  27887  ex-bc  27888  rmydioph  38550  expdiophlem2  38558  stoweidlem13  41167  fmtno5  42500  fmtnofac1  42513  31prm  42543  5odd  42654  sbgoldbo  42710