Metamath Proof Explorer

Syntax definition cmaxidl

Description: Extend class notation with the class of maximal ideals.

Ref Expression
Assertion cmaxidl class MaxIdl