Definition df-dmn

Description: Define the class of (integral) domains. A domain is a commutative prime ring. (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Assertion	df-dmn	|- Dmn = ( PrRing i^i Com2 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdmn	|- Dmn
1		cprrng	|- PrRing
2		ccm2	|- Com2
3	1 2	cin	|- ( PrRing i^i Com2 )
4	0 3	wceq	|- Dmn = ( PrRing i^i Com2 )