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 i^i Domn )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cidom 
 |-  IDomn
1 ccrg 
 |-  CRing
2 cdomn 
 |-  Domn
3 1 2 cin 
 |-  ( CRing i^i Domn )
4 0 3 wceq 
 |-  IDomn = ( CRing i^i Domn )