Description: Anintegral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | df-idom | ⊢ IDomn = ( CRing ∩ Domn ) |
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 ) |