Metamath Proof Explorer


Syntax definition caov

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 .

Ref Expression
Assertion caov
class (( A F B ))