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 IDomn
1 ccrg CRing
2 cdomn Domn
3 1 2 cin ( CRing ∩ Domn )
4 0 3 wceq IDomn = ( CRing ∩ Domn )