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

Definition df-5 9761
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 9752 . 2  class  5
2 c4 9751 . . 3  class  4
3 c1 8692 . . 3  class  1
4 caddc 8694 . . 3  class  +
52, 3, 4co 5778 . 2  class  ( 4  +  1 )
61, 5wceq 1619 1  wff  5  =  ( 4  +  1 )
Colors of variables: wff set class
This definition is referenced by:  5re  9775  5pos  9787  4p1e5  9802  3p2e5  9808  4p2e6  9810  5p5e10  9816  5nn  9833  4lt5  9845  6p5e11  10127  7p5e12  10130  8p5e13  10135  8p7e15  10137  9p5e14  10142  9p6e15  10143  5t5e25  10153  6t5e30  10157  7t5e35  10162  8t5e40  10168  9t5e45  10175  ef01bndlem  12412  5prm  13058  lt6abl  15129  log2ublem3  20192  ppiublem2  20390  bclbnd  20467  bposlem6  20476  bposlem9  20479  lgsdir2lem3  20512  rmydioph  26460  expdiophlem2  26468  stoweidlem13  27083
  Copyright terms: Public domain W3C validator