Metamath Proof Explorer

Theorem isdmn2

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

Ref Expression
Assertion isdmn2 
|- ( R e. Dmn <-> ( R e. PrRing /\ R e. CRingOps ) )

Proof

Step Hyp Ref Expression
1 isdmn 
 |-  ( R e. Dmn <-> ( R e. PrRing /\ R e. Com2 ) )
2 prrngorngo 
 |-  ( R e. PrRing -> R e. RingOps )
3 iscrngo 
 |-  ( R e. CRingOps <-> ( R e. RingOps /\ R e. Com2 ) )
4 3 baibr 
 |-  ( R e. RingOps -> ( R e. Com2 <-> R e. CRingOps ) )
5 2 4 syl 
 |-  ( R e. PrRing -> ( R e. Com2 <-> R e. CRingOps ) )
6 5 pm5.32i 
 |-  ( ( R e. PrRing /\ R e. Com2 ) <-> ( R e. PrRing /\ R e. CRingOps ) )
7 1 6 bitri 
 |-  ( R e. Dmn <-> ( R e. PrRing /\ R e. CRingOps ) )