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

Definition df-neg 7183
Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction () to prevent syntax ambiguity. See cneg 7181 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 7181 . 2 class -𝐴
3 cc0 6887 . . 3 class 0
4 cmin 7180 . . 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  7202  nfnegd  7205  csbnegg  7207  negcl  7209  neg0  7255  negid  7256  negsub  7257  subneg  7258  negneg  7259  negsubdi  7265  renegcl  7270  mulneg1  7390  ltneg  7455  leneg  7458  ixi  7572  0mnnnnn0  8212  fzshftral  8968  bernneq2  9344  cji  9476
  Copyright terms: Public domain W3C validator