Syntax Definition cneg 4090

Description: Extend class notation to include unary minus. The symbol - 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 a different symbols for unary minus (-) and subtraction cmin 4089 (−) to prevent syntax ambiguity. For example, looking at the syntax definition co 3001, 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, "(-A − B)" is unambiguous.

Hypothesis

Ref	Expression
cA	class A

Assertion

Ref	Expression
cneg	class -A

See definition df-neg 4135 for more information.

metamath.org