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 (( 𝐴 𝐹 𝐵 )) |