Syntax Definition co 7275

Description: Extend class notation to include the value of an operation 𝐹 (such as +) for two arguments 𝐴 and 𝐵. Note that the syntax is simply three class symbols in a row surrounded by parentheses. Since operation values are the only possible class expressions consisting of three class expressions in a row surrounded by parentheses, the syntax is unambiguous. (For an example of how syntax could become ambiguous if we are not careful, see the comment in cneg 11206.)

Hypotheses

Ref	Expression
cA	class 𝐴
cB	class 𝐵
cF	class 𝐹

Assertion

Ref	Expression
co	class (𝐴𝐹𝐵)

See definition df-ov 7278 for more information.