Syntax Definition caov 41195

Description: Extend class notation to include the value of an operation F (such as +) for two arguments A and B. 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 6653.

Hypotheses

Ref	Expression
cA	class A
cB	class B
cF	class F

Assertion

Ref	Expression
caov	class (( A F B))

See definition df-aov 41198 for more information.