Metamath Proof Explorer
Description: An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025)
|
|
Ref |
Expression |
|
Hypothesis |
idomringd.1 |
⊢ ( 𝜑 → 𝑅 ∈ IDomn ) |
|
Assertion |
idomdomd |
⊢ ( 𝜑 → 𝑅 ∈ Domn ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
idomringd.1 |
⊢ ( 𝜑 → 𝑅 ∈ IDomn ) |
2 |
|
df-idom |
⊢ IDomn = ( CRing ∩ Domn ) |
3 |
1 2
|
eleqtrdi |
⊢ ( 𝜑 → 𝑅 ∈ ( CRing ∩ Domn ) ) |
4 |
3
|
elin2d |
⊢ ( 𝜑 → 𝑅 ∈ Domn ) |