Theorem dfidom2

Description: Alternate definition of the class of integral domains. An integral domain is a commutative prime ring. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 27-Jun-2026)

	Ref	Expression
Assertion	dfidom2	|- IDomn = ( PrmRing i^i CRing )

Proof

Step	Hyp	Ref	Expression
1		df-idom	|- IDomn = ( CRing i^i Domn )
2	1	eleq2i	|- ( x e. IDomn <-> x e. ( CRing i^i Domn ) )
3		elin	|- ( x e. ( CRing i^i Domn ) <-> ( x e. CRing /\ x e. Domn ) )
4	3	biancomi	|- ( x e. ( CRing i^i Domn ) <-> ( x e. Domn /\ x e. CRing ) )
5	2 4	bitri	|- ( x e. IDomn <-> ( x e. Domn /\ x e. CRing ) )
6		crngprmringdom	|- ( x e. CRing -> ( x e. PrmRing <-> x e. Domn ) )
7	6	bicomd	|- ( x e. CRing -> ( x e. Domn <-> x e. PrmRing ) )
8	5 7	bianim	|- ( x e. IDomn <-> ( x e. PrmRing /\ x e. CRing ) )
9		elin	|- ( x e. ( PrmRing i^i CRing ) <-> ( x e. PrmRing /\ x e. CRing ) )
10	8 9	bitr4i	|- ( x e. IDomn <-> x e. ( PrmRing i^i CRing ) )
11	10	eqriv	|- IDomn = ( PrmRing i^i CRing )