Metamath Proof Explorer


Syntax definition csra

Description: Extend class notation with the subring algebra generator.

Ref Expression
Assertion csra class subringAlg