Metamath Proof Explorer


Syntax definition cprcof

Description: Extend class notation with pre-composition functors.

Ref Expression
Assertion cprcof class −∘F