Metamath Proof Explorer


Syntax definition crtrcl

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

Ref Expression
Assertion crtrcl class t*rec