Theorem opelcnvg

Description: Ordered-pair membership in converse relation. (Contributed by NM, 13-May-1999) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	opelcnvg	$$⊢\left(A\in C\wedge B\in D\right)\to \left(⟨A,B⟩\in R^{-1}\leftrightarrow ⟨B,A⟩\in R\right)$$

Proof

Step	Hyp	Ref	Expression
1		brcnvg	$$⊢\left(A\in C\wedge B\in D\right)\to \left(A{R}^{-1}B\leftrightarrow BRA\right)$$
2		df-br	$$⊢A{R}^{-1}B\leftrightarrow ⟨A,B⟩\in R^{-1}$$
3		df-br	$$⊢BRA\leftrightarrow ⟨B,A⟩\in R$$
4	1 2 3	3bitr3g	$$⊢\left(A\in C\wedge B\in D\right)\to \left(⟨A,B⟩\in R^{-1}\leftrightarrow ⟨B,A⟩\in R\right)$$