Theorem idomdomd 20824

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

Syntax hints:   → wi 4   ∈ wcel 2143   ∩ cin 3904  CRingccrg 20311  Domncdomn 20791  IDomncidom 20792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-idom 20795

This theorem is referenced by:  domnprodeq0  33599  idomrcan  33602  subridom  33606  fracfld  33629  rprmasso2  33816  1arithufdlem1  33834  1arithufdlem3  33836  dfufd2lem  33839  zringfrac  33844  deg1prod  33873  ply1dg3rt0irred  33874  m1pmeq  33875  mplidomlem  33917  vietadeg1  33968  assafld  34027  minplyirredlem  34100  minplyirred  34101  algextdeglem7  34113  algextdeglem8  34114  deg1gprod  42907  deg1pow  42908