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

Definition df-5 9809
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 9800 . 2  class  5
2 c4 9799 . . 3  class  4
3 c1 8740 . . 3  class  1
4 caddc 8742 . . 3  class  +
52, 3, 4co 5860 . 2  class  ( 4  +  1 )
61, 5wceq 1625 1  wff  5  =  ( 4  +  1 )
Colors of variables: wff set class
This definition is referenced by:  5re  9823  5pos  9835  4p1e5  9851  3p2e5  9857  4p2e6  9859  5p5e10  9865  5nn  9882  4lt5  9894  6p5e11  10176  7p5e12  10179  8p5e13  10184  8p7e15  10186  9p5e14  10191  9p6e15  10192  5t5e25  10202  6t5e30  10206  7t5e35  10211  8t5e40  10217  9t5e45  10224  ef01bndlem  12466  5prm  13112  lt6abl  15183  log2ublem3  20246  ppiublem2  20444  bclbnd  20521  bposlem6  20530  bposlem9  20533  lgsdir2lem3  20566  rmydioph  27118  expdiophlem2  27126  stoweidlem13  27773
  Copyright terms: Public domain W3C validator