| 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 20696 | . . 3 ⊢ IDomn = (CRing ∩ Domn) | |
| 3 | 1, 2 | eleqtrdi 2851 | . 2 ⊢ (𝜑 → 𝑅 ∈ (CRing ∩ Domn)) |
| 4 | 3 | elin2d 4205 | 1 ⊢ (𝜑 → 𝑅 ∈ Domn) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 ∩ cin 3950 CRingccrg 20231 Domncdomn 20692 IDomncidom 20693 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-in 3958 df-idom 20696 |
| This theorem is referenced by: idomrcan 33282 idomrcanOLD 33285 subridom 33289 fracfld 33310 rprmasso2 33554 1arithufdlem1 33572 1arithufdlem3 33574 dfufd2lem 33577 zringfrac 33582 ply1dg3rt0irred 33607 m1pmeq 33608 r1pid2OLD 33629 assafld 33688 minplyirredlem 33753 minplyirred 33754 algextdeglem7 33764 algextdeglem8 33765 deg1gprod 42141 deg1pow 42142 |
| Copyright terms: Public domain | W3C validator |