Syntax Definition cneg 5273

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 a different symbols for unary minus (-u) and subtraction cmin 5272 (-) to prevent syntax ambiguity. For example, looking at the syntax definition co 3954, 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, "(-uA - B)" is unambiguous.

Hypothesis

Ref	Expression
cA	class A

Assertion

Ref	Expression
cneg	class -uA

See definition df-neg 5338 for more information.

Copyright terms: Public domain