Metamath Proof Explorer


Syntax definition cmfitp

Description: The evaluation function derived from the interpretation.

Ref Expression
Assertion cmfitp
class mFromItp