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

Definition df-5 10092
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 10083 . 2  class  5
2 c4 10082 . . 3  class  4
3 c1 9022 . . 3  class  1
4 caddc 9024 . . 3  class  +
52, 3, 4co 6110 . 2  class  ( 4  +  1 )
61, 5wceq 1653 1  wff  5  =  ( 4  +  1 )
Colors of variables: wff set class
This definition is referenced by:  5re  10106  5pos  10118  4p1e5  10136  3p2e5  10142  4p2e6  10144  5p5e10  10150  5nn  10167  4lt5  10179  6p5e11  10463  7p5e12  10466  8p5e13  10471  8p7e15  10473  9p5e14  10478  9p6e15  10479  5t5e25  10489  6t5e30  10493  7t5e35  10498  8t5e40  10504  9t5e45  10511  ef01bndlem  12816  5prm  13462  lt6abl  15535  log2ublem3  20819  ppiublem2  21018  bclbnd  21095  bposlem6  21104  bposlem9  21107  lgsdir2lem3  21140  rmydioph  27123  expdiophlem2  27131  stoweidlem13  27776
  Copyright terms: Public domain W3C validator