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 ∩ CRing )

Proof

Step	Hyp	Ref	Expression
1		df-idom	⊢ IDomn = ( CRing ∩ Domn )
2	1	eleq2i	⊢ ( 𝑥 ∈ IDomn ↔ 𝑥 ∈ ( CRing ∩ Domn ) )
3		elin	⊢ ( 𝑥 ∈ ( CRing ∩ Domn ) ↔ ( 𝑥 ∈ CRing ∧ 𝑥 ∈ Domn ) )
4	3	biancomi	⊢ ( 𝑥 ∈ ( CRing ∩ Domn ) ↔ ( 𝑥 ∈ Domn ∧ 𝑥 ∈ CRing ) )
5	2 4	bitri	⊢ ( 𝑥 ∈ IDomn ↔ ( 𝑥 ∈ Domn ∧ 𝑥 ∈ CRing ) )
6		crngprmringdom	⊢ ( 𝑥 ∈ CRing → ( 𝑥 ∈ PrmRing ↔ 𝑥 ∈ Domn ) )
7	6	bicomd	⊢ ( 𝑥 ∈ CRing → ( 𝑥 ∈ Domn ↔ 𝑥 ∈ PrmRing ) )
8	5 7	bianim	⊢ ( 𝑥 ∈ IDomn ↔ ( 𝑥 ∈ PrmRing ∧ 𝑥 ∈ CRing ) )
9		elin	⊢ ( 𝑥 ∈ ( PrmRing ∩ CRing ) ↔ ( 𝑥 ∈ PrmRing ∧ 𝑥 ∈ CRing ) )
10	8 9	bitr4i	⊢ ( 𝑥 ∈ IDomn ↔ 𝑥 ∈ ( PrmRing ∩ CRing ) )
11	10	eqriv	⊢ IDomn = ( PrmRing ∩ CRing )