MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cneg Unicode version

Syntax Definition cneg 9038
Description: Extend class notation to include unary minus. The symbol  -u is not a class by itself but part of a compound class definition. We do this rather than making it a formal function since it is so commonly used. Note: We use different symbols for unary minus ( -u) and subtraction cmin 9037 ( -) to prevent syntax ambiguity. For example, looking at the syntax definition co 5858, if we used the same symbol then " (  -  A  -  B ) " could mean either " -  A " minus " B", or it could represent the (meaningless) operation of classes " - " and " -  B " connected with "operation" " A". On the other hand, " ( -u A  -  B ) " is unambiguous.
Ref Expression
cA  class  A
Ref Expression
cneg  class  -u A

See definition df-neg 9040 for more information.

Colors of variables: wff set class
  Copyright terms: Public domain W3C validator