Metamath Proof Explorer

Syntax definition cmxidl

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

Ref Expression
Assertion cmxidl class MaxIdeal