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

Definition df-5 9897
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 9888 . 2  class  5
2 c4 9887 . . 3  class  4
3 c1 8828 . . 3  class  1
4 caddc 8830 . . 3  class  +
52, 3, 4co 5945 . 2  class  ( 4  +  1 )
61, 5wceq 1642 1  wff  5  =  ( 4  +  1 )
Colors of variables: wff set class
This definition is referenced by:  5re  9911  5pos  9923  4p1e5  9941  3p2e5  9947  4p2e6  9949  5p5e10  9955  5nn  9972  4lt5  9984  6p5e11  10266  7p5e12  10269  8p5e13  10274  8p7e15  10276  9p5e14  10281  9p6e15  10282  5t5e25  10292  6t5e30  10296  7t5e35  10301  8t5e40  10307  9t5e45  10314  ef01bndlem  12561  5prm  13207  lt6abl  15280  log2ublem3  20355  ppiublem2  20554  bclbnd  20631  bposlem6  20640  bposlem9  20643  lgsdir2lem3  20676  rmydioph  26430  expdiophlem2  26438  stoweidlem13  27085
  Copyright terms: Public domain W3C validator