MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  idomdomd Structured version   Visualization version   GIF version

Theorem idomdomd 20726
Description: An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025.)
Hypothesis
Ref Expression
idomringd.1 (𝜑𝑅 ∈ IDomn)
Assertion
Ref Expression
idomdomd (𝜑𝑅 ∈ Domn)

Proof of Theorem idomdomd
StepHypRef Expression
1 idomringd.1 . . 3 (𝜑𝑅 ∈ IDomn)
2 df-idom 20696 . . 3 IDomn = (CRing ∩ Domn)
31, 2eleqtrdi 2851 . 2 (𝜑𝑅 ∈ (CRing ∩ Domn))
43elin2d 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