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

Definition df-5 8168
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 8159 . 2  class  5
2 c4 8158 . . 3  class  4
3 c1 7044 . . 3  class  1
4 caddc 7046 . . 3  class  +
52, 3, 4co 5543 . 2  class  ( 4  +  1 )
61, 5wceq 1285 1  wff  5  =  ( 4  +  1 )
Colors of variables: wff set class
This definition is referenced by:  5re  8185  5pos  8206  4p1e5  8235  3p2e5  8240  4p2e6  8242  5nn  8263  4lt5  8274  5p5e10  8628  6p5e11  8630  7p5e12  8634  8p5e13  8640  8p7e15  8642  9p5e14  8647  9p6e15  8648  5t5e25  8660  6t5e30  8664  7t5e35  8669  8t5e40  8675  9t5e45  8682  fldiv4p1lem1div2  9387  ex-fac  10716  ex-bc  10717
  Copyright terms: Public domain W3C validator