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	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 ◡ 𝑅 𝐵 ↔ 𝐵 𝑅 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑥 = 𝐴 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝐴 ) )
2		breq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 𝑅 𝐴 ↔ 𝐵 𝑅 𝐴 ) )
3		df-cnv	⊢ ◡ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 𝑅 𝑥 }
4	1 2 3	brabg	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 ◡ 𝑅 𝐵 ↔ 𝐵 𝑅 𝐴 ) )