Theorem isidom2

Description: The predicate "is an integral domain": An integral domain is a commutative prime ring. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 27-Jun-2026)

	Ref	Expression
Assertion	isidom2	⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ PrmRing ∧ 𝑅 ∈ CRing ) )

Proof

Step	Hyp	Ref	Expression
1		dfidom2	⊢ IDomn = ( PrmRing ∩ CRing )
2	1	elin2	⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ PrmRing ∧ 𝑅 ∈ CRing ) )