Theorem idomdomd 20986

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ∩ cin 4088  CRingccrg 20469  Domncdomn 20953  IDomncidom 20954

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 4090  df-idom 20957

This theorem is used by:  domnprodeq0  33890  idomrcan  33893  subridom  33897  fracfld  33920  rprmasso2  34108  1arithufdlem1  34126  1arithufdlem3  34128  dfufd2lem  34131  zringfrac  34136  deg1prod  34165  ply1dg3rt0irred  34166  m1pmeq  34167  mplidomlem  34209  vietadeg1  34260  assafld  34319  minplyirredlem  34392  minplyirred  34393  algextdeglem7  34405  algextdeglem8  34406  deg1gprod  43299  deg1pow  43300