Theorem idomcringd 20987

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 20988. (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 20957	. . 3 ⊢ IDomn = (CRing ∩ Domn)
3	1, 2	eleqtrdi 2870	. 2 ⊢ (𝜑 → 𝑅 ∈ (CRing ∩ Domn))
4	3	elin1d 4100	1 ⊢ (𝜑 → 𝑅 ∈ CRing)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ∩ cin 4088  CRingccrg 20469  Domncdomn 20953  IDomncidom 20954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4090  df-idom 20957

This theorem is used by:  idomringd  20988  domnprodeq0  33890  subridom  33897  fracfld  33920  idomsubr  33921  dvdsruasso2  33991  mxidlirredi  34046  mxidlirred  34047  rprmasso  34107  rprmasso2  34108  rprmirredlem  34112  rprmirred  34113  rprmirredb  34114  1arithidomlem1  34117  1arithidom  34119  pidufd  34125  1arithufdlem1  34126  1arithufdlem3  34128  1arithufdlem4  34129  dfufd2lem  34131  zringfrac  34136  deg1prod  34165  ply1dg3rt0irred  34166  mplidomlem  34209  vietadeg1  34260  vietalem  34261  vieta  34262  assafld  34319  fldextrspunfld  34358  unitscyglem5  43386  aks5lem7  43387