Metamath Proof Explorer

Syntax definition crngoiso

Description: Extend class notation with the class of ring isomorphisms.

Ref Expression
Assertion crngoiso class RingOpsIso