Metamath Proof Explorer
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 |
|
Detailed syntax breakdown
Step |
Hyp |
Ref |
Expression |
0 |
|
cdmn |
|
1 |
|
cprrng |
|
2 |
|
ccm2 |
|
3 |
1 2
|
cin |
|
4 |
0 3
|
wceq |
|