Theorem idomcringd 20810

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

Syntax hints:   → wi 4   ∈ wcel 2149   ∩ cin 3912  CRingccrg 20315  Domncdomn 20776  IDomncidom 20777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-idom 20780

This theorem is referenced by:  idomringd  20811  domnprodeq0  33539  subridom  33546  fracfld  33571  idomsubr  33572  dvdsruasso2  33642  mxidlirredi  33698  mxidlirred  33699  rprmasso  33759  rprmasso2  33760  rprmirredlem  33764  rprmirred  33765  rprmirredb  33766  1arithidomlem1  33769  1arithidom  33771  pidufd  33777  1arithufdlem1  33778  1arithufdlem3  33780  1arithufdlem4  33781  dfufd2lem  33783  zringfrac  33788  deg1prod  33817  ply1dg3rt0irred  33818  mplidomlem  33861  vietadeg1  33912  vietalem  33913  vieta  33914  assafld  33971  fldextrspunfld  34010  unitscyglem5  42855  aks5lem7  42856