Theorem idomdomd 20970

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ∩ cin 3898  CRingccrg 20453  Domncdomn 20937  IDomncidom 20938

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-idom 20941

This theorem is used by:  domnprodeq0  33833  idomrcan  33836  subridom  33840  fracfld  33863  rprmasso2  34051  1arithufdlem1  34069  1arithufdlem3  34071  dfufd2lem  34074  zringfrac  34079  deg1prod  34108  ply1dg3rt0irred  34109  m1pmeq  34110  mplidomlem  34152  vietadeg1  34203  assafld  34262  minplyirredlem  34335  minplyirred  34336  algextdeglem7  34348  algextdeglem8  34349  deg1gprod  43170  deg1pow  43171