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

Definition df-neg 6982
Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction () to prevent syntax ambiguity. See cneg 6980 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 6980 . 2 class -A
3 cc0 6711 . . 3 class 0
4 cmin 6979 . . 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  7001  nfnegd  7004  csbnegg  7006  negcl  7008  neg0  7053  negid  7054  negsub  7055  subneg  7056  negneg  7057  negsubdi  7063  renegcl  7068  mulneg1  7188  ltneg  7252  leneg  7255  ixi  7367  0mnnnnn0  7990  fzshftral  8740  bernneq2  9023  cji  9130
  Copyright terms: Public domain W3C validator