Syntax Definition caov 44497

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 a pair of parentheses in contrast to the current definition, see df-ov 7258.

Hypotheses

Ref	Expression
cA	class 𝐴
cB	class 𝐵
cF	class 𝐹

Assertion

Ref	Expression
caov	class ((𝐴𝐹𝐵))

See definition df-aov 44500 for more information.