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

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

Detailed syntax breakdown of Definition df-neg
StepHypRef Expression
1 cA . . 3  class  A
21cneg 7902 . 2  class  -u A
3 cc0 7588 . . 3  class  0
4 cmin 7901 . . 3  class  -
53, 1, 4co 5742 . 2  class  ( 0  -  A )
62, 5wceq 1316 1  wff  -u A  =  ( 0  -  A )
Colors of variables: wff set class
This definition is referenced by:  negeq  7923  nfnegd  7926  csbnegg  7928  negcl  7930  neg0  7976  negid  7977  negsub  7978  subneg  7979  negneg  7980  negsubdi  7986  renegcl  7991  mulneg1  8125  ltneg  8192  leneg  8195  ixi  8312  0mnnnnn0  8967  fzshftral  9843  bernneq2  10368  cji  10629  bdtri  10966  sin0pilem1  12773  cospi  12792  coshalfpip  12814  ptolemy  12816
  Copyright terms: Public domain W3C validator