Theorem brcnvg

Description: The converse of a binary relation swaps arguments. Theorem 11 of Suppes p. 61. (Contributed by NM, 10-Oct-2005)

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

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢x=A\to \left(yRx\leftrightarrow yRA\right)$$
2		breq1	$$⊢y=B\to \left(yRA\leftrightarrow BRA\right)$$
3		df-cnv	$$⊢R^{-1}=\left\{⟨x,y⟩|yRx\right\}$$
4	1 2 3	brabg	$$⊢\left(A\in C\wedge B\in D\right)\to \left(A{R}^{-1}B\leftrightarrow BRA\right)$$