Theorem idomdomd 20646

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 20616	. . 3 ⊢ IDomn = (CRing ∩ Domn)
3	1, 2	eleqtrdi 2838	. 2 ⊢ (𝜑 → 𝑅 ∈ (CRing ∩ Domn))
4	3	elin2d 4164	1 ⊢ (𝜑 → 𝑅 ∈ Domn)

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3910  CRingccrg 20154  Domncdomn 20612  IDomncidom 20613

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918  df-idom 20616

This theorem is referenced by:  idomrcan  33245  idomrcanOLD  33248  subridom  33252  fracfld  33274  rprmasso2  33490  1arithufdlem1  33508  1arithufdlem3  33510  dfufd2lem  33513  zringfrac  33518  ply1dg3rt0irred  33544  m1pmeq  33545  r1pid2OLD  33567  assafld  33626  minplyirredlem  33693  minplyirred  33694  algextdeglem7  33706  algextdeglem8  33707  deg1gprod  42121  deg1pow  42122