Description: Swap the members of an ordered pair. (Contributed by NM, 14-Dec-2008) (Revised by Mario Carneiro, 30-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | opswap | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvsng | |
|
2 | 1 | unieqd | |
3 | opex | |
|
4 | 3 | unisn | |
5 | 2 4 | eqtrdi | |
6 | uni0 | |
|
7 | opprc | |
|
8 | 7 | sneqd | |
9 | 8 | cnveqd | |
10 | cnvsn0 | |
|
11 | 9 10 | eqtrdi | |
12 | 11 | unieqd | |
13 | ancom | |
|
14 | opprc | |
|
15 | 13 14 | sylnbi | |
16 | 6 12 15 | 3eqtr4a | |
17 | 5 16 | pm2.61i | |