Theorem idomcringd 20825

Description: An integral domain is a commutative ring with unity. (Contributed by Thierry Arnoux, 4-May-2025.) Formerly subproof of idomringd 20826. (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 20795	. . 3 ⊢ IDomn = (CRing ∩ Domn)
3	1, 2	eleqtrdi 2873	. 2 ⊢ (𝜑 → 𝑅 ∈ (CRing ∩ Domn))
4	3	elin1d 4157	1 ⊢ (𝜑 → 𝑅 ∈ CRing)

Syntax hints:   → wi 4   ∈ wcel 2143   ∩ cin 3904  CRingccrg 20311  Domncdomn 20791  IDomncidom 20792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-idom 20795

This theorem is referenced by:  idomringd  20826  domnprodeq0  33599  subridom  33606  fracfld  33629  idomsubr  33630  dvdsruasso2  33699  mxidlirredi  33754  mxidlirred  33755  rprmasso  33815  rprmasso2  33816  rprmirredlem  33820  rprmirred  33821  rprmirredb  33822  1arithidomlem1  33825  1arithidom  33827  pidufd  33833  1arithufdlem1  33834  1arithufdlem3  33836  1arithufdlem4  33837  dfufd2lem  33839  zringfrac  33844  deg1prod  33873  ply1dg3rt0irred  33874  mplidomlem  33917  vietadeg1  33968  vietalem  33969  vieta  33970  assafld  34027  fldextrspunfld  34066  unitscyglem5  42966  aks5lem7  42967