Metamath Proof Explorer


Theorem relbrtpos

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

Ref Expression
Assertion relbrtpos Rel F A B tpos F C B A F C

Proof

Step Hyp Ref Expression
1 reltpos Rel tpos F
2 1 a1i Rel F Rel tpos F
3 brrelex2 Rel tpos F A B tpos F C C V
4 2 3 sylan Rel F A B tpos F C C V
5 brrelex2 Rel F B A F C C V
6 brtpos C V A B tpos F C B A F C
7 4 5 6 pm5.21nd Rel F A B tpos F C B A F C