Metamath Proof Explorer


Theorem tposoprab

Description: Transposition of a class of ordered triples. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Hypothesis tposoprab.1 F = x y z | φ
Assertion tposoprab tpos F = y x z | φ

Proof

Step Hyp Ref Expression
1 tposoprab.1 F = x y z | φ
2 1 tposeqi tpos F = tpos x y z | φ
3 reldmoprab Rel dom x y z | φ
4 dftpos3 Rel dom x y z | φ tpos x y z | φ = a b c | b a x y z | φ c
5 3 4 ax-mp tpos x y z | φ = a b c | b a x y z | φ c
6 nfcv _ y b a
7 nfoprab2 _ y x y z | φ
8 nfcv _ y c
9 6 7 8 nfbr y b a x y z | φ c
10 nfcv _ x b a
11 nfoprab1 _ x x y z | φ
12 nfcv _ x c
13 10 11 12 nfbr x b a x y z | φ c
14 nfv a x y x y z | φ c
15 nfv b x y x y z | φ c
16 opeq12 b = x a = y b a = x y
17 16 ancoms a = y b = x b a = x y
18 17 breq1d a = y b = x b a x y z | φ c x y x y z | φ c
19 9 13 14 15 18 cbvoprab12 a b c | b a x y z | φ c = y x c | x y x y z | φ c
20 nfcv _ z x y
21 nfoprab3 _ z x y z | φ
22 nfcv _ z c
23 20 21 22 nfbr z x y x y z | φ c
24 nfv c φ
25 breq2 c = z x y x y z | φ c x y x y z | φ z
26 df-br x y x y z | φ z x y z x y z | φ
27 oprabidw x y z x y z | φ φ
28 26 27 bitri x y x y z | φ z φ
29 25 28 bitrdi c = z x y x y z | φ c φ
30 23 24 29 cbvoprab3 y x c | x y x y z | φ c = y x z | φ
31 19 30 eqtri a b c | b a x y z | φ c = y x z | φ
32 2 5 31 3eqtri tpos F = y x z | φ