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

Definition df-5 9986
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 9977 . 2  class  5
2 c4 9976 . . 3  class  4
3 c1 8917 . . 3  class  1
4 caddc 8919 . . 3  class  +
52, 3, 4co 6013 . 2  class  ( 4  +  1 )
61, 5wceq 1649 1  wff  5  =  ( 4  +  1 )
Colors of variables: wff set class
This definition is referenced by:  5re  10000  5pos  10012  4p1e5  10030  3p2e5  10036  4p2e6  10038  5p5e10  10044  5nn  10061  4lt5  10073  6p5e11  10357  7p5e12  10360  8p5e13  10365  8p7e15  10367  9p5e14  10372  9p6e15  10373  5t5e25  10383  6t5e30  10387  7t5e35  10392  8t5e40  10398  9t5e45  10405  ef01bndlem  12705  5prm  13351  lt6abl  15424  log2ublem3  20648  ppiublem2  20847  bclbnd  20924  bposlem6  20933  bposlem9  20936  lgsdir2lem3  20969  rmydioph  26769  expdiophlem2  26777  stoweidlem13  27423
  Copyright terms: Public domain W3C validator