Metamath Proof Explorer


Syntax definition chof

Description: Extend class notation with the Hom functor.

Ref Expression
Assertion chof class HomF