Metamath Proof Explorer


Theorem opswap

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 AB-1=BA

Proof

Step Hyp Ref Expression
1 cnvsng AVBVAB-1=BA
2 1 unieqd AVBVAB-1=BA
3 opex BAV
4 3 unisn BA=BA
5 2 4 eqtrdi AVBVAB-1=BA
6 uni0 =
7 opprc ¬AVBVAB=
8 7 sneqd ¬AVBVAB=
9 8 cnveqd ¬AVBVAB-1=-1
10 cnvsn0 -1=
11 9 10 eqtrdi ¬AVBVAB-1=
12 11 unieqd ¬AVBVAB-1=
13 ancom AVBVBVAV
14 opprc ¬BVAVBA=
15 13 14 sylnbi ¬AVBVBA=
16 6 12 15 3eqtr4a ¬AVBVAB-1=BA
17 5 16 pm2.61i AB-1=BA