Theorem idomdomd 20978

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ∩ cin 4089  CRingccrg 20461  Domncdomn 20945  IDomncidom 20946

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4091  df-idom 20949

This theorem is used by:  domnprodeq0  33883  idomrcan  33886  subridom  33890  fracfld  33913  rprmasso2  34101  1arithufdlem1  34119  1arithufdlem3  34121  dfufd2lem  34124  zringfrac  34129  deg1prod  34158  ply1dg3rt0irred  34159  m1pmeq  34160  mplidomlem  34202  vietadeg1  34253  assafld  34312  minplyirredlem  34385  minplyirred  34386  algextdeglem7  34398  algextdeglem8  34399  deg1gprod  43234  deg1pow  43235