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

Definition df-neg 6962
Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction () to prevent syntax ambiguity. See cneg 6960 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 6960 . 2 class -A
3 cc0 6691 . . 3 class 0
4 cmin 6959 . . 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  6981  nfnegd  6984  csbnegg  6986  negcl  6988  neg0  7033  negid  7034  negsub  7035  subneg  7036  negneg  7037  negsubdi  7043  renegcl  7048  mulneg1  7168  ltneg  7232  leneg  7235  ixi  7347  0mnnnnn0  7970  fzshftral  8720  bernneq2  9003  cji  9110
  Copyright terms: Public domain W3C validator