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

Definition df-neg 7600
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 7598 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 7598 . 2  class  -u A
3 cc0 7294 . . 3  class  0
4 cmin 7597 . . 3  class  -
53, 1, 4co 5613 . 2  class  ( 0  -  A )
62, 5wceq 1287 1  wff  -u A  =  ( 0  -  A )
Colors of variables: wff set class
This definition is referenced by:  negeq  7619  nfnegd  7622  csbnegg  7624  negcl  7626  neg0  7672  negid  7673  negsub  7674  subneg  7675  negneg  7676  negsubdi  7682  renegcl  7687  mulneg1  7817  ltneg  7884  leneg  7887  ixi  8001  0mnnnnn0  8638  fzshftral  9452  bernneq2  9972  cji  10232
  Copyright terms: Public domain W3C validator