Definition df-dmn

Description: Obsolete definition, use df-idom resp. dfidom2 instead. Define the class of (integral) domains. A domain is a commutative prime ring. (Contributed by Jeff Madsen, 10-Jun-2010) (New usage is discouraged.)

	Ref	Expression
Assertion	df-dmn	$$⊢\mathrm{Dmn}=\mathrm{PrRing}\cap \mathrm{Com2}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdmn	$$class\mathrm{Dmn}$$
1		cprrng	$$class\mathrm{PrRing}$$
2		ccm2	$$class\mathrm{Com2}$$
3	1 2	cin	$$class\left(\mathrm{PrRing}\cap \mathrm{Com2}\right)$$
4	0 3	wceq	$$wff\mathrm{Dmn}=\mathrm{PrRing}\cap \mathrm{Com2}$$