Theorem idomdomd 20659

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

Syntax hints:   → wi 4   ∈ wcel 2113   ∩ cin 3900  CRingccrg 20169  Domncdomn 20625  IDomncidom 20626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-idom 20629

This theorem is referenced by:  domnprodeq0  33358  idomrcan  33361  idomrcanOLD  33364  subridom  33368  fracfld  33390  rprmasso2  33607  1arithufdlem1  33625  1arithufdlem3  33627  dfufd2lem  33630  zringfrac  33635  deg1prod  33664  ply1dg3rt0irred  33665  m1pmeq  33666  r1pid2OLD  33690  vietadeg1  33734  assafld  33794  minplyirredlem  33867  minplyirred  33868  algextdeglem7  33880  algextdeglem8  33881  deg1gprod  42394  deg1pow  42395