Metamath Proof Explorer

Theorem isdmn

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

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

Proof

Step Hyp Ref Expression
1 df-dmn 
 |-  Dmn = ( PrRing i^i Com2 )
2 1 elin2 
 |-  ( R e. Dmn <-> ( R e. PrRing /\ R e. Com2 ) )