# Metamath Proof Explorer

## Theorem isdmn2

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

Ref Expression
Assertion isdmn2 ${⊢}{R}\in \mathrm{Dmn}↔\left({R}\in \mathrm{PrRing}\wedge {R}\in \mathrm{CRingOps}\right)$

### Proof

Step Hyp Ref Expression
1 isdmn ${⊢}{R}\in \mathrm{Dmn}↔\left({R}\in \mathrm{PrRing}\wedge {R}\in \mathrm{Com2}\right)$
2 prrngorngo ${⊢}{R}\in \mathrm{PrRing}\to {R}\in \mathrm{RingOps}$
3 iscrngo ${⊢}{R}\in \mathrm{CRingOps}↔\left({R}\in \mathrm{RingOps}\wedge {R}\in \mathrm{Com2}\right)$
4 3 baibr ${⊢}{R}\in \mathrm{RingOps}\to \left({R}\in \mathrm{Com2}↔{R}\in \mathrm{CRingOps}\right)$
5 2 4 syl ${⊢}{R}\in \mathrm{PrRing}\to \left({R}\in \mathrm{Com2}↔{R}\in \mathrm{CRingOps}\right)$
6 5 pm5.32i ${⊢}\left({R}\in \mathrm{PrRing}\wedge {R}\in \mathrm{Com2}\right)↔\left({R}\in \mathrm{PrRing}\wedge {R}\in \mathrm{CRingOps}\right)$
7 1 6 bitri ${⊢}{R}\in \mathrm{Dmn}↔\left({R}\in \mathrm{PrRing}\wedge {R}\in \mathrm{CRingOps}\right)$