Theorem relbrtpos

Description: The transposition swaps arguments of a three-parameter relation. (Contributed by Mario Carneiro, 3-Nov-2015)

	Ref	Expression
Assertion	relbrtpos	⊢ ( Rel 𝐹 → ( ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		reltpos	⊢ Rel tpos 𝐹
2	1	a1i	⊢ ( Rel 𝐹 → Rel tpos 𝐹 )
3		brrelex2	⊢ ( ( Rel tpos 𝐹 ∧ ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ) → 𝐶 ∈ V )
4	2 3	sylan	⊢ ( ( Rel 𝐹 ∧ ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ) → 𝐶 ∈ V )
5		brrelex2	⊢ ( ( Rel 𝐹 ∧ ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ) → 𝐶 ∈ V )
6		brtpos	⊢ ( 𝐶 ∈ V → ( ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ) )
7	4 5 6	pm5.21nd	⊢ ( Rel 𝐹 → ( ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ) )