Theorem idomdomd 20809

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

Syntax hints:   → wi 4   ∈ wcel 2149   ∩ cin 3912  CRingccrg 20315  Domncdomn 20776  IDomncidom 20777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-idom 20780

This theorem is referenced by:  domnprodeq0  33539  idomrcan  33542  subridom  33546  fracfld  33571  rprmasso2  33760  1arithufdlem1  33778  1arithufdlem3  33780  dfufd2lem  33783  zringfrac  33788  deg1prod  33817  ply1dg3rt0irred  33818  m1pmeq  33819  mplidomlem  33861  vietadeg1  33912  assafld  33971  minplyirredlem  34044  minplyirred  34045  algextdeglem7  34057  algextdeglem8  34058  deg1gprod  42796  deg1pow  42797