Theorem idomdomd 20874

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ∩ cin 3905  CRingccrg 20360  Domncdomn 20841  IDomncidom 20842

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913  df-idom 20845

This theorem is used by:  domnprodeq0  33663  idomrcan  33666  subridom  33670  fracfld  33693  rprmasso2  33880  1arithufdlem1  33898  1arithufdlem3  33900  dfufd2lem  33903  zringfrac  33908  deg1prod  33937  ply1dg3rt0irred  33938  m1pmeq  33939  mplidomlem  33981  vietadeg1  34032  assafld  34091  minplyirredlem  34164  minplyirred  34165  algextdeglem7  34177  algextdeglem8  34178  deg1gprod  42965  deg1pow  42966