Database
BASIC ALGEBRAIC STRUCTURES
Rings
Left regular elements and domains
idomdomd
Next ⟩
idomcringd
Metamath Proof Explorer
Ascii
Unicode
Theorem
idomdomd
Description:
An integral domain is a domain.
(Contributed by
Thierry Arnoux
, 22-Mar-2025)
Ref
Expression
Hypothesis
idomringd.1
⊢
φ
→
R
∈
IDomn
Assertion
idomdomd
⊢
φ
→
R
∈
Domn
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
elin2d
⊢
φ
→
R
∈
Domn