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 ∩ Com2 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdmn	⊢ Dmn
1		cprrng	⊢ PrRing
2		ccm2	⊢ Com2
3	1 2	cin	⊢ ( PrRing ∩ Com2 )
4	0 3	wceq	⊢ Dmn = ( PrRing ∩ Com2 )