Metamath Proof Explorer


Syntax definition crtrcl

Description: Extend class notation with recursively defined reflexive, transitive closure.

Ref Expression
Assertion crtrcl
class t*rec