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 | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 〈 𝐴 , 𝐵 〉 ∈ ◡ 𝑅 ↔ 〈 𝐵 , 𝐴 〉 ∈ 𝑅 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brcnvg | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 ◡ 𝑅 𝐵 ↔ 𝐵 𝑅 𝐴 ) ) | |
2 | df-br | ⊢ ( 𝐴 ◡ 𝑅 𝐵 ↔ 〈 𝐴 , 𝐵 〉 ∈ ◡ 𝑅 ) | |
3 | df-br | ⊢ ( 𝐵 𝑅 𝐴 ↔ 〈 𝐵 , 𝐴 〉 ∈ 𝑅 ) | |
4 | 1 2 3 | 3bitr3g | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 〈 𝐴 , 𝐵 〉 ∈ ◡ 𝑅 ↔ 〈 𝐵 , 𝐴 〉 ∈ 𝑅 ) ) |