Definition df-idom

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

	Ref	Expression
Assertion	df-idom	|- IDomn = ( CRing i^i Domn )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cidom	|- IDomn
1		ccrg	|- CRing
2		cdomn	|- Domn
3	1 2	cin	|- ( CRing i^i Domn )
4	0 3	wceq	|- IDomn = ( CRing i^i Domn )