Theorem isdmn2

Description: The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Assertion	isdmn2	⊢ ( 𝑅 ∈ Dmn ↔ ( 𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps ) )

Proof

Step	Hyp	Ref	Expression
1		isdmn	⊢ ( 𝑅 ∈ Dmn ↔ ( 𝑅 ∈ PrRing ∧ 𝑅 ∈ Com2 ) )
2		prrngorngo	⊢ ( 𝑅 ∈ PrRing → 𝑅 ∈ RingOps )
3		iscrngo	⊢ ( 𝑅 ∈ CRingOps ↔ ( 𝑅 ∈ RingOps ∧ 𝑅 ∈ Com2 ) )
4	3	baibr	⊢ ( 𝑅 ∈ RingOps → ( 𝑅 ∈ Com2 ↔ 𝑅 ∈ CRingOps ) )
5	2 4	syl	⊢ ( 𝑅 ∈ PrRing → ( 𝑅 ∈ Com2 ↔ 𝑅 ∈ CRingOps ) )
6	5	pm5.32i	⊢ ( ( 𝑅 ∈ PrRing ∧ 𝑅 ∈ Com2 ) ↔ ( 𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps ) )
7	1 6	bitri	⊢ ( 𝑅 ∈ Dmn ↔ ( 𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps ) )