Theorem idomdomd 20642

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3916  CRingccrg 20150  Domncdomn 20608  IDomncidom 20609

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924  df-idom 20612

This theorem is referenced by:  idomrcan  33236  idomrcanOLD  33239  subridom  33243  fracfld  33265  rprmasso2  33504  1arithufdlem1  33522  1arithufdlem3  33524  dfufd2lem  33527  zringfrac  33532  ply1dg3rt0irred  33558  m1pmeq  33559  r1pid2OLD  33581  assafld  33640  minplyirredlem  33707  minplyirred  33708  algextdeglem7  33720  algextdeglem8  33721  deg1gprod  42135  deg1pow  42136