Metamath Proof Explorer


Syntax definition csubrng

Description: Extend class notation with all subrings of a non-unital ring.

Ref Expression
Assertion csubrng class SubRng