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

Definition df-neg 6942
Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction () to prevent syntax ambiguity. See cneg 6940 for a discussion of this. (Contributed by NM, 10-Feb-1995.)
Assertion
Ref Expression
df-neg -A = (0 − A)

Detailed syntax breakdown of Definition df-neg
StepHypRef Expression
1 cA . . 3 class A
21cneg 6940 . 2 class -A
3 cc0 6671 . . 3 class 0
4 cmin 6939 . . 3 class
53, 1, 4co 5455 . 2 class (0 − A)
62, 5wceq 1242 1 wff -A = (0 − A)
Colors of variables: wff set class
This definition is referenced by:  negeq  6961  nfnegd  6964  csbnegg  6966  negcl  6968  neg0  7013  negid  7014  negsub  7015  subneg  7016  negneg  7017  negsubdi  7023  renegcl  7028  mulneg1  7148  ltneg  7212  leneg  7215  ixi  7327  0mnnnnn0  7950  fzshftral  8700  bernneq2  8983  cji  9090
  Copyright terms: Public domain W3C validator