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

Definition df-neg 7929
Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction () to prevent syntax ambiguity. See cneg 7927 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 7927 . 2 class -𝐴
3 cc0 7613 . . 3 class 0
4 cmin 7926 . . 3 class
53, 1, 4co 5767 . 2 class (0 − 𝐴)
62, 5wceq 1331 1 wff -𝐴 = (0 − 𝐴)
Colors of variables: wff set class
This definition is referenced by:  negeq  7948  nfnegd  7951  csbnegg  7953  negcl  7955  neg0  8001  negid  8002  negsub  8003  subneg  8004  negneg  8005  negsubdi  8011  renegcl  8016  mulneg1  8150  ltneg  8217  leneg  8220  ixi  8338  0mnnnnn0  9002  fzshftral  9881  bernneq2  10406  cji  10667  bdtri  11004  sin0pilem1  12851  cospi  12870  coshalfpip  12892  ptolemy  12894
  Copyright terms: Public domain W3C validator