Description: An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025)
Ref | Expression | ||
---|---|---|---|
Hypothesis | idomringd.1 | |- ( ph -> R e. IDomn ) |
|
Assertion | idomdomd | |- ( ph -> R e. Domn ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idomringd.1 | |- ( ph -> R e. IDomn ) |
|
2 | df-idom | |- IDomn = ( CRing i^i Domn ) |
|
3 | 1 2 | eleqtrdi | |- ( ph -> R e. ( CRing i^i Domn ) ) |
4 | 3 | elin2d | |- ( ph -> R e. Domn ) |