Metamath Proof Explorer

Theorem isdmn2

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

Ref Expression
Assertion isdmn2 ⊢R∈Dmn↔R∈PrRing∧R∈CRingOps

Proof

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