Metamath Proof Explorer


Syntax definition cref

Description: Extend class definition to include the refinement relation.

Ref Expression
Assertion cref
class Ref