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

Definition df-neg 8050
Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction () to prevent syntax ambiguity. See cneg 8048 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 8048 . 2 class -𝐴
3 cc0 7733 . . 3 class 0
4 cmin 8047 . . 3 class
53, 1, 4co 5825 . 2 class (0 − 𝐴)
62, 5wceq 1335 1 wff -𝐴 = (0 − 𝐴)
Colors of variables: wff set class
This definition is referenced by:  negeq  8069  nfnegd  8072  csbnegg  8074  negcl  8076  neg0  8122  negid  8123  negsub  8124  subneg  8125  negneg  8126  negsubdi  8132  renegcl  8137  mulneg1  8271  ltneg  8338  leneg  8341  ixi  8459  0mnnnnn0  9123  fzshftral  10011  bernneq2  10543  cji  10806  bdtri  11143  prmdiv  12114  sin0pilem1  13144  cospi  13163  coshalfpip  13185  ptolemy  13187  logbrec  13319
  Copyright terms: Public domain W3C validator