Theorem idomdomd 20726

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

Syntax hints:   → wi 4   ∈ wcel 2100   ∩ cin 3958  CRingccrg 20239  Domncdomn 20692  IDomncidom 20693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-v 3474  df-in 3966  df-idom 20696

This theorem is referenced by:  idomrcan  33161  idomrcanOLD  33164  subridom  33168  fracfld  33188  rprmasso2  33432  1arithufdlem1  33450  1arithufdlem3  33452  dfufd2lem  33455  zringfrac  33460  ply1dg3rt0irred  33485  m1pmeq  33486  r1pid2OLD  33507  minplyirredlem  33610  minplyirred  33611  algextdeglem7  33621  algextdeglem8  33622  deg1gprod  41886  deg1pow  41887