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 )