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 )) |