Database
REAL AND COMPLEX NUMBERS
Reflexive and transitive closures of relations
Reflexive-transitive closure as an indexed union
crtrcl
Next ⟩
df-rtrclrec
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
crtrcl
Description:
Extend class notation with recursively defined reflexive, transitive closure.
Ref
Expression
Assertion
crtrcl
$${class}\mathrm{t*rec}$$