Metamath Proof Explorer


Syntax definition ctrs

Description: Extend the definition of a class to include the transitivity class (but cf. the transitive class defined in df-tr ).

Ref Expression
Assertion ctrs class Trs