Metamath Proof Explorer


Syntax definition cevlf

Description: Extend class notation with the evaluation functor.

Ref Expression
Assertion cevlf class eval F