This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )