Theorem idomcringd 20889

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ∩ cin 3898  CRingccrg 20374  Domncdomn 20855  IDomncidom 20856

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906  df-idom 20859

This theorem is used by:  idomringd  20890  domnprodeq0  33720  subridom  33727  fracfld  33750  idomsubr  33751  dvdsruasso2  33820  mxidlirredi  33875  mxidlirred  33876  rprmasso  33936  rprmasso2  33937  rprmirredlem  33941  rprmirred  33942  rprmirredb  33943  1arithidomlem1  33946  1arithidom  33948  pidufd  33954  1arithufdlem1  33955  1arithufdlem3  33957  1arithufdlem4  33958  dfufd2lem  33960  zringfrac  33965  deg1prod  33994  ply1dg3rt0irred  33995  mplidomlem  34038  vietadeg1  34089  vietalem  34090  vieta  34091  assafld  34148  fldextrspunfld  34187  unitscyglem5  43066  aks5lem7  43067