Theorem opprdomn

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

	Ref	Expression
Hypothesis	opprdomn.1	⊢ 𝑂 = ( oppr ‘ 𝑅 )
Assertion	opprdomn	⊢ ( 𝑅 ∈ Domn → 𝑂 ∈ Domn )

Proof

Step	Hyp	Ref	Expression
1		opprdomn.1	⊢ 𝑂 = ( oppr ‘ 𝑅 )
2	1	opprdomnb	⊢ ( 𝑅 ∈ Domn ↔ 𝑂 ∈ Domn )
3	2	biimpi	⊢ ( 𝑅 ∈ Domn → 𝑂 ∈ Domn )