MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-5 Unicode version

Definition df-5 10017
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
StepHypRef Expression
1 c5 10008 . 2  class  5
2 c4 10007 . . 3  class  4
3 c1 8947 . . 3  class  1
4 caddc 8949 . . 3  class  +
52, 3, 4co 6040 . 2  class  ( 4  +  1 )
61, 5wceq 1649 1  wff  5  =  ( 4  +  1 )
Colors of variables: wff set class
This definition is referenced by:  5re  10031  5pos  10043  4p1e5  10061  3p2e5  10067  4p2e6  10069  5p5e10  10075  5nn  10092  4lt5  10104  6p5e11  10388  7p5e12  10391  8p5e13  10396  8p7e15  10398  9p5e14  10403  9p6e15  10404  5t5e25  10414  6t5e30  10418  7t5e35  10423  8t5e40  10429  9t5e45  10436  ef01bndlem  12740  5prm  13386  lt6abl  15459  log2ublem3  20741  ppiublem2  20940  bclbnd  21017  bposlem6  21026  bposlem9  21029  lgsdir2lem3  21062  rmydioph  26975  expdiophlem2  26983  stoweidlem13  27629
  Copyright terms: Public domain W3C validator