Metamath Proof Explorer


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