Metamath Proof Explorer


Syntax definition coe

Description: Extend the definition of a class to include the ordinal exponentiation operation.

Ref Expression
Assertion coe class o