Metamath Proof Explorer


Theorem idomdomd

Description: An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypothesis idomringd.1 φ R IDomn
Assertion idomdomd φ R Domn

Proof

Step Hyp Ref Expression
1 idomringd.1 φ R IDomn
2 df-idom IDomn = CRing Domn
3 1 2 eleqtrdi φ R CRing Domn
4 3 elin2d φ R Domn