Description: The transposition swaps the first two elements in a collection of ordered triples. (Contributed by Mario Carneiro, 1-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | ottpos |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brtpos | ||
2 | df-br | ||
3 | df-br | ||
4 | 1 2 3 | 3bitr3g | |
5 | df-ot | ||
6 | 5 | eleq1i | |
7 | df-ot | ||
8 | 7 | eleq1i | |
9 | 4 6 8 | 3bitr4g |