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  8313  0mnnnnn0  8977  fzshftral  9856  bernneq2  10381  cji  10642  bdtri  10979  sin0pilem1  12789  cospi  12808  coshalfpip  12830  ptolemy  12832
  Copyright terms: Public domain W3C validator