Metamath Proof Explorer


Theorem idomcringd

Description: An integral domain is a commutative ring with unity. (Contributed by Thierry Arnoux, 4-May-2025) Formerly subproof of idomringd . (Proof shortened by SN, 14-May-2025)

Ref Expression
Hypothesis idomringd.1 φ R IDomn
Assertion idomcringd φ R CRing

Proof

Step Hyp Ref Expression
1 idomringd.1 φ R IDomn
2 df-idom IDomn = CRing Domn
3 1 2 eleqtrdi φ R CRing Domn
4 3 elin1d φ R CRing