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

Definition df-neg 7185
Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction () to prevent syntax ambiguity. See cneg 7183 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 7183 . 2 class -𝐴
3 cc0 6889 . . 3 class 0
4 cmin 7182 . . 3 class
53, 1, 4co 5512 . 2 class (0 − 𝐴)
62, 5wceq 1243 1 wff -𝐴 = (0 − 𝐴)
Colors of variables: wff set class
This definition is referenced by:  negeq  7204  nfnegd  7207  csbnegg  7209  negcl  7211  neg0  7257  negid  7258  negsub  7259  subneg  7260  negneg  7261  negsubdi  7267  renegcl  7272  mulneg1  7392  ltneg  7457  leneg  7460  ixi  7574  0mnnnnn0  8214  fzshftral  8970  bernneq2  9370  cji  9502
  Copyright terms: Public domain W3C validator