Theorem idomcringd 20700

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

Syntax hints:   → wi 4   ∈ wcel 2099   ∩ cin 3947  CRingccrg 20212  Domncdomn 20665  IDomncidom 20666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3466  df-in 3955  df-idom 20669

This theorem is referenced by:  idomringd  20701  subridom  33142  fracfld  33162  idomsubr  33163  dvdsruasso2  33266  rsprprmprmidlb  33403  rprmasso  33405  rprmasso2  33406  rprmirredlem  33410  rprmirred  33411  rprmirredb  33412  1arithidomlem1  33415  1arithidom  33417  1arithufdlem1  33424  1arithufdlem3  33426  1arithufdlem4  33427  dfufd2lem  33429  zringfrac  33434  ply1dg3rt0irred  33459