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

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

Detailed syntax breakdown of Definition df-neg
StepHypRef Expression
1 cA . . 3 class 𝐴
21cneg 7601 . 2 class -𝐴
3 cc0 7297 . . 3 class 0
4 cmin 7600 . . 3 class
53, 1, 4co 5615 . 2 class (0 − 𝐴)
62, 5wceq 1287 1 wff -𝐴 = (0 − 𝐴)
Colors of variables: wff set class
This definition is referenced by:  negeq  7622  nfnegd  7625  csbnegg  7627  negcl  7629  neg0  7675  negid  7676  negsub  7677  subneg  7678  negneg  7679  negsubdi  7685  renegcl  7690  mulneg1  7820  ltneg  7887  leneg  7890  ixi  8004  0mnnnnn0  8641  fzshftral  9455  bernneq2  9975  cji  10235
  Copyright terms: Public domain W3C validator