Description: The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010)
Ref | Expression | ||
---|---|---|---|
Assertion | isdmn | ⊢ ( 𝑅 ∈ Dmn ↔ ( 𝑅 ∈ PrRing ∧ 𝑅 ∈ Com2 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-dmn | ⊢ Dmn = ( PrRing ∩ Com2 ) | |
2 | 1 | elin2 | ⊢ ( 𝑅 ∈ Dmn ↔ ( 𝑅 ∈ PrRing ∧ 𝑅 ∈ Com2 ) ) |