Definition df-idom

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

	Ref	Expression
Assertion	df-idom	$$⊢\mathrm{IDomn}=\mathrm{CRing}\cap \mathrm{Domn}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cidom	$$class\mathrm{IDomn}$$
1		ccrg	$$class\mathrm{CRing}$$
2		cdomn	$$class\mathrm{Domn}$$
3	1 2	cin	$$class\left(\mathrm{CRing}\cap \mathrm{Domn}\right)$$
4	0 3	wceq	$$wff\mathrm{IDomn}=\mathrm{CRing}\cap \mathrm{Domn}$$