Metamath Proof Explorer


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 class Dmn
1 cprrng class PrRing
2 ccm2 class Com2
3 1 2 cin class PrRing Com2
4 0 3 wceq wff Dmn = PrRing Com2