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

Definition df-5 10021
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 10012 . 2  class  5
2 c4 10011 . . 3  class  4
3 c1 8951 . . 3  class  1
4 caddc 8953 . . 3  class  +
52, 3, 4co 6044 . 2  class  ( 4  +  1 )
61, 5wceq 1649 1  wff  5  =  ( 4  +  1 )
Colors of variables: wff set class
This definition is referenced by:  5re  10035  5pos  10047  4p1e5  10065  3p2e5  10071  4p2e6  10073  5p5e10  10079  5nn  10096  4lt5  10108  6p5e11  10392  7p5e12  10395  8p5e13  10400  8p7e15  10402  9p5e14  10407  9p6e15  10408  5t5e25  10418  6t5e30  10422  7t5e35  10427  8t5e40  10433  9t5e45  10440  ef01bndlem  12744  5prm  13390  lt6abl  15463  log2ublem3  20745  ppiublem2  20944  bclbnd  21021  bposlem6  21030  bposlem9  21033  lgsdir2lem3  21066  rmydioph  26979  expdiophlem2  26987  stoweidlem13  27633
  Copyright terms: Public domain W3C validator