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=xyz|φ
Assertion tposoprab tposF=yxz|φ

Proof

Step Hyp Ref Expression
1 tposoprab.1 F=xyz|φ
2 1 tposeqi tposF=tposxyz|φ
3 reldmoprab Reldomxyz|φ
4 dftpos3 Reldomxyz|φtposxyz|φ=abc|baxyz|φc
5 3 4 ax-mp tposxyz|φ=abc|baxyz|φc
6 nfcv _yba
7 nfoprab2 _yxyz|φ
8 nfcv _yc
9 6 7 8 nfbr ybaxyz|φc
10 nfcv _xba
11 nfoprab1 _xxyz|φ
12 nfcv _xc
13 10 11 12 nfbr xbaxyz|φc
14 nfv axyxyz|φc
15 nfv bxyxyz|φc
16 opeq12 b=xa=yba=xy
17 16 ancoms a=yb=xba=xy
18 17 breq1d a=yb=xbaxyz|φcxyxyz|φc
19 9 13 14 15 18 cbvoprab12 abc|baxyz|φc=yxc|xyxyz|φc
20 nfcv _zxy
21 nfoprab3 _zxyz|φ
22 nfcv _zc
23 20 21 22 nfbr zxyxyz|φc
24 nfv cφ
25 breq2 c=zxyxyz|φcxyxyz|φz
26 df-br xyxyz|φzxyzxyz|φ
27 oprabidw xyzxyz|φφ
28 26 27 bitri xyxyz|φzφ
29 25 28 bitrdi c=zxyxyz|φcφ
30 23 24 29 cbvoprab3 yxc|xyxyz|φc=yxz|φ
31 19 30 eqtri abc|baxyz|φc=yxz|φ
32 2 5 31 3eqtri tposF=yxz|φ