Theorem idomdomd 20703

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3888  CRingccrg 20215  Domncdomn 20669  IDomncidom 20670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-idom 20673

This theorem is referenced by:  domnprodeq0  33337  idomrcan  33340  idomrcanOLD  33343  subridom  33347  fracfld  33369  rprmasso2  33586  1arithufdlem1  33604  1arithufdlem3  33606  dfufd2lem  33609  zringfrac  33614  deg1prod  33643  ply1dg3rt0irred  33644  m1pmeq  33645  r1pid2OLD  33669  vietadeg1  33722  assafld  33781  minplyirredlem  33854  minplyirred  33855  algextdeglem7  33867  algextdeglem8  33868  deg1gprod  42579  deg1pow  42580