Theorem idomcringd 20875

Description: An integral domain is a commutative ring with unity. (Contributed by Thierry Arnoux, 4-May-2025.) Formerly subproof of idomringd 20876. (Proof shortened by SN, 14-May-2025.)

Hypothesis

Ref	Expression
idomringd.1	⊢ (𝜑 → 𝑅 ∈ IDomn)

Assertion

Ref	Expression
idomcringd	⊢ (𝜑 → 𝑅 ∈ CRing)

Proof of Theorem idomcringd

Step	Hyp	Ref	Expression
1		idomringd.1	. . 3 ⊢ (𝜑 → 𝑅 ∈ IDomn)
2		df-idom 20845	. . 3 ⊢ IDomn = (CRing ∩ Domn)
3	1, 2	eleqtrdi 2875	. 2 ⊢ (𝜑 → 𝑅 ∈ (CRing ∩ Domn))
4	3	elin1d 4157	1 ⊢ (𝜑 → 𝑅 ∈ CRing)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ∩ cin 3905  CRingccrg 20360  Domncdomn 20841  IDomncidom 20842

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913  df-idom 20845

This theorem is used by:  idomringd  20876  domnprodeq0  33663  subridom  33670  fracfld  33693  idomsubr  33694  dvdsruasso2  33763  mxidlirredi  33818  mxidlirred  33819  rprmasso  33879  rprmasso2  33880  rprmirredlem  33884  rprmirred  33885  rprmirredb  33886  1arithidomlem1  33889  1arithidom  33891  pidufd  33897  1arithufdlem1  33898  1arithufdlem3  33900  1arithufdlem4  33901  dfufd2lem  33903  zringfrac  33908  deg1prod  33937  ply1dg3rt0irred  33938  mplidomlem  33981  vietadeg1  34032  vietalem  34033  vieta  34034  assafld  34091  fldextrspunfld  34130  unitscyglem5  43024  aks5lem7  43025