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	|- ( R e. IDomn <-> ( R e. PrmRing /\ R e. CRing ) )

Proof

Step	Hyp	Ref	Expression
1		dfidom2	|- IDomn = ( PrmRing i^i CRing )
2	1	elin2	|- ( R e. IDomn <-> ( R e. PrmRing /\ R e. CRing ) )