ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-5 Unicode version

Definition df-5 8640
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 8632 . 2  class  5
2 c4 8631 . . 3  class  4
3 c1 7501 . . 3  class  1
4 caddc 7503 . . 3  class  +
52, 3, 4co 5706 . 2  class  ( 4  +  1 )
61, 5wceq 1299 1  wff  5  =  ( 4  +  1 )
Colors of variables: wff set class
This definition is referenced by:  5re  8657  5pos  8678  4p1e5  8708  3p2e5  8713  4p2e6  8715  5nn  8736  4lt5  8747  5p5e10  9104  6p5e11  9106  7p5e12  9110  8p5e13  9116  8p7e15  9118  9p5e14  9123  9p6e15  9124  5t5e25  9136  6t5e30  9140  7t5e35  9145  8t5e40  9151  9t5e45  9158  fldiv4p1lem1div2  9919  ef01bndlem  11261  ex-exp  12542  ex-fac  12543  ex-bc  12544
  Copyright terms: Public domain W3C validator