Description: Transposition of a class of ordered triples. (Contributed by Mario Carneiro, 10-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | tposoprab.1 | |
|
Assertion | tposoprab | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tposoprab.1 | |
|
2 | 1 | tposeqi | |
3 | reldmoprab | |
|
4 | dftpos3 | |
|
5 | 3 4 | ax-mp | |
6 | nfcv | |
|
7 | nfoprab2 | |
|
8 | nfcv | |
|
9 | 6 7 8 | nfbr | |
10 | nfcv | |
|
11 | nfoprab1 | |
|
12 | nfcv | |
|
13 | 10 11 12 | nfbr | |
14 | nfv | |
|
15 | nfv | |
|
16 | opeq12 | |
|
17 | 16 | ancoms | |
18 | 17 | breq1d | |
19 | 9 13 14 15 18 | cbvoprab12 | |
20 | nfcv | |
|
21 | nfoprab3 | |
|
22 | nfcv | |
|
23 | 20 21 22 | nfbr | |
24 | nfv | |
|
25 | breq2 | |
|
26 | df-br | |
|
27 | oprabidw | |
|
28 | 26 27 | bitri | |
29 | 25 28 | bitrdi | |
30 | 23 24 29 | cbvoprab3 | |
31 | 19 30 | eqtri | |
32 | 2 5 31 | 3eqtri | |