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 e. IDomn <-> ( R e. CRing /\ R e. Domn ) )

Proof

Step Hyp Ref Expression
1 df-idom 
 |-  IDomn = ( CRing i^i Domn )
2 1 elin2 
 |-  ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )