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

Proof

Step	Hyp	Ref	Expression
1		brcnvg	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 ◡ 𝑅 𝐵 ↔ 𝐵 𝑅 𝐴 ) )
2		df-br	⊢ ( 𝐴 ◡ 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ 𝑅 )
3		df-br	⊢ ( 𝐵 𝑅 𝐴 ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ 𝑅 )
4	1 2 3	3bitr3g	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ 𝑅 ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ 𝑅 ) )