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

Definition df-neg 8080
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 8078 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 8078 . 2  class  -u A
3 cc0 7761 . . 3  class  0
4 cmin 8077 . . 3  class  -
53, 1, 4co 5850 . 2  class  ( 0  -  A )
62, 5wceq 1348 1  wff  -u A  =  ( 0  -  A )
Colors of variables: wff set class
This definition is referenced by:  negeq  8099  nfnegd  8102  csbnegg  8104  negcl  8106  neg0  8152  negid  8153  negsub  8154  subneg  8155  negneg  8156  negsubdi  8162  renegcl  8167  mulneg1  8301  ltneg  8368  leneg  8371  ixi  8489  0mnnnnn0  9154  fzshftral  10051  bernneq2  10584  cji  10853  bdtri  11190  prmdiv  12176  pcrec  12249  pcid  12264  4sqlem6  12322  4sqlem10  12326  sin0pilem1  13455  cospi  13474  coshalfpip  13496  ptolemy  13498  logbrec  13631  lgslem4  13657
  Copyright terms: Public domain W3C validator