![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > idomdomd | Structured version Visualization version GIF version |
Description: An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
Ref | Expression |
---|---|
idomringd.1 | ⊢ (𝜑 → 𝑅 ∈ IDomn) |
Ref | Expression |
---|---|
idomdomd | ⊢ (𝜑 → 𝑅 ∈ Domn) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idomringd.1 | . . 3 ⊢ (𝜑 → 𝑅 ∈ IDomn) | |
2 | df-idom 20718 | . . 3 ⊢ IDomn = (CRing ∩ Domn) | |
3 | 1, 2 | eleqtrdi 2854 | . 2 ⊢ (𝜑 → 𝑅 ∈ (CRing ∩ Domn)) |
4 | 3 | elin2d 4228 | 1 ⊢ (𝜑 → 𝑅 ∈ Domn) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2108 ∩ cin 3975 CRingccrg 20261 Domncdomn 20714 IDomncidom 20715 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2711 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1778 df-sb 2065 df-clab 2718 df-cleq 2732 df-clel 2819 df-v 3490 df-in 3983 df-idom 20718 |
This theorem is referenced by: idomrcan 33248 idomrcanOLD 33251 subridom 33255 fracfld 33275 rprmasso2 33519 1arithufdlem1 33537 1arithufdlem3 33539 dfufd2lem 33542 zringfrac 33547 ply1dg3rt0irred 33572 m1pmeq 33573 r1pid2OLD 33594 assafld 33650 minplyirredlem 33703 minplyirred 33704 algextdeglem7 33714 algextdeglem8 33715 deg1gprod 42097 deg1pow 42098 |
Copyright terms: Public domain | W3C validator |