Metamath Proof Explorer


Syntax definition cj

Description: Extend the definition of a class to include an order isomorphism from ( On X. On ) X. 9o to On .

Ref Expression
Assertion cj
class _J