Metamath Proof Explorer

Theorem isidom

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

Ref Expression
Assertion isidom ⊢R∈IDomn↔R∈CRing∧R∈Domn

Proof

Step Hyp Ref Expression
1 df-idom ⊢IDomn=CRing∩Domn
2 1 elin2 ⊢R∈IDomn↔R∈CRing∧R∈Domn