Theorem idomdomd 20684

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3925  CRingccrg 20192  Domncdomn 20650  IDomncidom 20651

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933  df-idom 20654

This theorem is referenced by:  idomrcan  33219  idomrcanOLD  33222  subridom  33226  fracfld  33248  rprmasso2  33487  1arithufdlem1  33505  1arithufdlem3  33507  dfufd2lem  33510  zringfrac  33515  ply1dg3rt0irred  33541  m1pmeq  33542  r1pid2OLD  33564  assafld  33623  minplyirredlem  33690  minplyirred  33691  algextdeglem7  33703  algextdeglem8  33704  deg1gprod  42099  deg1pow  42100