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 2851	. 2 ⊢ (𝜑 → 𝑅 ∈ (CRing ∩ Domn))
4	3	elin2d 4205	1 ⊢ (𝜑 → 𝑅 ∈ Domn)

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3950  CRingccrg 20231  Domncdomn 20692  IDomncidom 20693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-idom 20696

This theorem is referenced by:  idomrcan  33282  idomrcanOLD  33285  subridom  33289  fracfld  33310  rprmasso2  33554  1arithufdlem1  33572  1arithufdlem3  33574  dfufd2lem  33577  zringfrac  33582  ply1dg3rt0irred  33607  m1pmeq  33608  r1pid2OLD  33629  assafld  33688  minplyirredlem  33753  minplyirred  33754  algextdeglem7  33764  algextdeglem8  33765  deg1gprod  42141  deg1pow  42142