Database
REAL AND COMPLEX NUMBERS
Reflexive and transitive closures of relations
Exponentiation of relations
crelexp
Next ⟩
df-relexp
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
crelexp
Description:
Extend class notation to include relation exponentiation.
Ref
Expression
Assertion
crelexp
$${class}{\uparrow}_{r}$$