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	Could not format assertion : No typesetting found for |- ( R e. IDomn <-> ( R e. PrmRing /\ R e. CRing ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dfidom2	Could not format IDomn = ( PrmRing i^i CRing ) : No typesetting found for |- IDomn = ( PrmRing i^i CRing ) with typecode |-
2	1	elin2	Could not format ( R e. IDomn <-> ( R e. PrmRing /\ R e. CRing ) ) : No typesetting found for |- ( R e. IDomn <-> ( R e. PrmRing /\ R e. CRing ) ) with typecode |-