Theorem opprdomn

Description: The opposite of a domain is also a domain. (Contributed by Mario Carneiro, 15-Jun-2015)

	Ref	Expression
Hypothesis	opprdomn.1	$$⊢O={opp}_r\left(R\right)$$
Assertion	opprdomn	$$⊢R\in \mathrm{Domn}\to O\in \mathrm{Domn}$$

Proof

Step	Hyp	Ref	Expression
1		opprdomn.1	$$⊢O={opp}_r\left(R\right)$$
2	1	opprdomnb	$$⊢R\in \mathrm{Domn}\leftrightarrow O\in \mathrm{Domn}$$
3	2	biimpi	$$⊢R\in \mathrm{Domn}\to O\in \mathrm{Domn}$$