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

Definition df-neg 8162
Description: Define the negative of a number (unary minus). We use different symbols for unary minus ( -u) and subtraction ( -) to prevent syntax ambiguity. See cneg 8160 for a discussion of this. (Contributed by NM, 10-Feb-1995.)
Assertion
Ref Expression
df-neg  |-  -u A  =  ( 0  -  A )

Detailed syntax breakdown of Definition df-neg
StepHypRef Expression
1 cA . . 3  class  A
21cneg 8160 . 2  class  -u A
3 cc0 7842 . . 3  class  0
4 cmin 8159 . . 3  class  -
53, 1, 4co 5897 . 2  class  ( 0  -  A )
62, 5wceq 1364 1  wff  -u A  =  ( 0  -  A )
Colors of variables: wff set class
This definition is referenced by:  negeq  8181  nfnegd  8184  csbnegg  8186  negcl  8188  neg0  8234  negid  8235  negsub  8236  subneg  8237  negneg  8238  negsubdi  8244  renegcl  8249  mulneg1  8383  ltneg  8450  leneg  8453  ixi  8571  0mnnnnn0  9239  fzshftral  10140  bernneq2  10676  cji  10946  bdtri  11283  prmdiv  12270  pcrec  12343  pcid  12359  4sqlem6  12418  4sqlem10  12422  sin0pilem1  14679  cospi  14698  coshalfpip  14720  ptolemy  14722  logbrec  14855  lgslem4  14882
  Copyright terms: Public domain W3C validator