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

Definition df-neg 7248
Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction () to prevent syntax ambiguity. See cneg 7246 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 7246 . 2 class -𝐴
3 cc0 6947 . . 3 class 0
4 cmin 7245 . . 3 class
53, 1, 4co 5540 . 2 class (0 − 𝐴)
62, 5wceq 1259 1 wff -𝐴 = (0 − 𝐴)
Colors of variables: wff set class
This definition is referenced by:  negeq  7267  nfnegd  7270  csbnegg  7272  negcl  7274  neg0  7320  negid  7321  negsub  7322  subneg  7323  negneg  7324  negsubdi  7330  renegcl  7335  mulneg1  7464  ltneg  7531  leneg  7534  ixi  7648  0mnnnnn0  8271  fzshftral  9072  bernneq2  9538  cji  9730
  Copyright terms: Public domain W3C validator