Metamath Proof Explorer


Syntax definition cretr

Description: Extend class notation with the retract relation.

Ref Expression
Assertion cretr class Retr