Metamath Proof Explorer


Syntax definition crestrict

Description: Declare the syntax for the restriction function.

Ref Expression
Assertion crestrict class Restrict