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

Definition df-5 9803
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 9794 . 2  class  5
2 c4 9793 . . 3  class  4
3 c1 8734 . . 3  class  1
4 caddc 8736 . . 3  class  +
52, 3, 4co 5820 . 2  class  ( 4  +  1 )
61, 5wceq 1623 1  wff  5  =  ( 4  +  1 )
Colors of variables: wff set class
This definition is referenced by:  5re  9817  5pos  9829  4p1e5  9845  3p2e5  9851  4p2e6  9853  5p5e10  9859  5nn  9876  4lt5  9888  6p5e11  10170  7p5e12  10173  8p5e13  10178  8p7e15  10180  9p5e14  10185  9p6e15  10186  5t5e25  10196  6t5e30  10200  7t5e35  10205  8t5e40  10211  9t5e45  10218  ef01bndlem  12460  5prm  13106  lt6abl  15177  log2ublem3  20240  ppiublem2  20438  bclbnd  20515  bposlem6  20524  bposlem9  20527  lgsdir2lem3  20560  rmydioph  26518  expdiophlem2  26526  stoweidlem13  27173
  Copyright terms: Public domain W3C validator