Metamath Proof Explorer


Syntax definition cof

Description: Extend class notation to include mapping of an operation to a function operation.

Ref Expression
Assertion cof class f R