Theorem idomdomd 20641

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

Step	Hyp	Ref	Expression
1		idomringd.1	. . 3 ⊢ (𝜑 → 𝑅 ∈ IDomn)
2		df-idom 20611	. . 3 ⊢ IDomn = (CRing ∩ Domn)
3	1, 2	eleqtrdi 2841	. 2 ⊢ (𝜑 → 𝑅 ∈ (CRing ∩ Domn))
4	3	elin2d 4152	1 ⊢ (𝜑 → 𝑅 ∈ Domn)

Syntax hints:   → wi 4   ∈ wcel 2111   ∩ cin 3896  CRingccrg 20152  Domncdomn 20607  IDomncidom 20608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904  df-idom 20611

This theorem is referenced by:  idomrcan  33245  idomrcanOLD  33248  subridom  33252  fracfld  33274  rprmasso2  33491  1arithufdlem1  33509  1arithufdlem3  33511  dfufd2lem  33514  zringfrac  33519  ply1dg3rt0irred  33546  m1pmeq  33547  r1pid2OLD  33569  assafld  33650  minplyirredlem  33723  minplyirred  33724  algextdeglem7  33736  algextdeglem8  33737  deg1gprod  42181  deg1pow  42182