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