Metamath Proof Explorer

Syntax definition cidom

Description: Class of integral domains.

Ref Expression
Assertion cidom 
class IDomn