Metamath Proof Explorer


Theorem idomdomd

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 )