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

Definition df-5 9687
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 9678 . 2  class  5
2 c4 9677 . . 3  class  4
3 c1 8618 . . 3  class  1
4 caddc 8620 . . 3  class  +
52, 3, 4co 5710 . 2  class  ( 4  +  1 )
61, 5wceq 1619 1  wff  5  =  ( 4  +  1 )
Colors of variables: wff set class
This definition is referenced by:  5re  9701  5pos  9713  4p1e5  9728  3p2e5  9734  4p2e6  9736  5p5e10  9742  5nn  9759  4lt5  9771  6p5e11  10053  7p5e12  10056  8p5e13  10061  8p7e15  10063  9p5e14  10068  9p6e15  10069  5t5e25  10079  6t5e30  10083  7t5e35  10088  8t5e40  10094  9t5e45  10101  ef01bndlem  12338  5prm  12984  lt6abl  15016  log2ublem3  20076  ppiublem2  20274  bclbnd  20351  bposlem6  20360  bposlem9  20363  lgsdir2lem3  20396  rmydioph  26273  expdiophlem2  26281
  Copyright terms: Public domain W3C validator