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

Definition df-5 9807
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 9798 . 2  class  5
2 c4 9797 . . 3  class  4
3 c1 8738 . . 3  class  1
4 caddc 8740 . . 3  class  +
52, 3, 4co 5858 . 2  class  ( 4  +  1 )
61, 5wceq 1623 1  wff  5  =  ( 4  +  1 )
Colors of variables: wff set class
This definition is referenced by:  5re  9821  5pos  9833  4p1e5  9849  3p2e5  9855  4p2e6  9857  5p5e10  9863  5nn  9880  4lt5  9892  6p5e11  10174  7p5e12  10177  8p5e13  10182  8p7e15  10184  9p5e14  10189  9p6e15  10190  5t5e25  10200  6t5e30  10204  7t5e35  10209  8t5e40  10215  9t5e45  10222  ef01bndlem  12464  5prm  13110  lt6abl  15181  log2ublem3  20244  ppiublem2  20442  bclbnd  20519  bposlem6  20528  bposlem9  20531  lgsdir2lem3  20564  rmydioph  27107  expdiophlem2  27115  stoweidlem13  27762
  Copyright terms: Public domain W3C validator