Theorem idomdomd 20742

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

Syntax hints:   → wi 4   ∈ wcel 2105   ∩ cin 3961  CRingccrg 20251  Domncdomn 20708  IDomncidom 20709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969  df-idom 20712

This theorem is referenced by:  idomrcan  33262  idomrcanOLD  33265  subridom  33269  fracfld  33289  rprmasso2  33533  1arithufdlem1  33551  1arithufdlem3  33553  dfufd2lem  33556  zringfrac  33561  ply1dg3rt0irred  33586  m1pmeq  33587  r1pid2OLD  33608  assafld  33664  minplyirredlem  33717  minplyirred  33718  algextdeglem7  33728  algextdeglem8  33729  deg1gprod  42121  deg1pow  42122