Theorem idomcringd 20978

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ∩ cin 3898  CRingccrg 20460  Domncdomn 20944  IDomncidom 20945

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-idom 20948

This theorem is used by:  idomringd  20979  domnprodeq0  33840  subridom  33847  fracfld  33870  idomsubr  33871  dvdsruasso2  33941  mxidlirredi  33996  mxidlirred  33997  rprmasso  34057  rprmasso2  34058  rprmirredlem  34062  rprmirred  34063  rprmirredb  34064  1arithidomlem1  34067  1arithidom  34069  pidufd  34075  1arithufdlem1  34076  1arithufdlem3  34078  1arithufdlem4  34079  dfufd2lem  34081  zringfrac  34086  deg1prod  34115  ply1dg3rt0irred  34116  mplidomlem  34159  vietadeg1  34210  vietalem  34211  vieta  34212  assafld  34269  fldextrspunfld  34308  unitscyglem5  43249  aks5lem7  43250