Metamath Proof Explorer


Definition df-idom

Description: Anintegral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015)

Ref Expression
Assertion df-idom IDomn = CRing Domn

Detailed syntax breakdown

Step Hyp Ref Expression
0 cidom class IDomn
1 ccrg class CRing
2 cdomn class Domn
3 1 2 cin class CRing Domn
4 0 3 wceq wff IDomn = CRing Domn