Metamath Proof Explorer


Syntax definition ctrpred

Description: Define the transitive predecessor class as a class.

Ref Expression
Assertion ctrpred
class TrPred ( R , A , X )