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 
|- U. `' { <. A , B >. } = <. B , A >.

Proof

Step Hyp Ref Expression
1 cnvsng 
 |-  ( ( A e. _V /\ B e. _V ) -> `' { <. A , B >. } = { <. B , A >. } )
2 1 unieqd 
 |-  ( ( A e. _V /\ B e. _V ) -> U. `' { <. A , B >. } = U. { <. B , A >. } )
3 opex 
 |-  <. B , A >. e. _V
4 3 unisn 
 |-  U. { <. B , A >. } = <. B , A >.
5 2 4 eqtrdi 
 |-  ( ( A e. _V /\ B e. _V ) -> U. `' { <. A , B >. } = <. B , A >. )
6 uni0 
 |-  U. (/) = (/)
7 opprc 
 |-  ( -. ( A e. _V /\ B e. _V ) -> <. A , B >. = (/) )
8 7 sneqd 
 |-  ( -. ( A e. _V /\ B e. _V ) -> { <. A , B >. } = { (/) } )
9 8 cnveqd 
 |-  ( -. ( A e. _V /\ B e. _V ) -> `' { <. A , B >. } = `' { (/) } )
10 cnvsn0 
 |-  `' { (/) } = (/)
11 9 10 eqtrdi 
 |-  ( -. ( A e. _V /\ B e. _V ) -> `' { <. A , B >. } = (/) )
12 11 unieqd 
 |-  ( -. ( A e. _V /\ B e. _V ) -> U. `' { <. A , B >. } = U. (/) )
13 ancom 
 |-  ( ( A e. _V /\ B e. _V ) <-> ( B e. _V /\ A e. _V ) )
14 opprc 
 |-  ( -. ( B e. _V /\ A e. _V ) -> <. B , A >. = (/) )
15 13 14 sylnbi 
 |-  ( -. ( A e. _V /\ B e. _V ) -> <. B , A >. = (/) )
16 6 12 15 3eqtr4a 
 |-  ( -. ( A e. _V /\ B e. _V ) -> U. `' { <. A , B >. } = <. B , A >. )
17 5 16 pm2.61i 
 |-  U. `' { <. A , B >. } = <. B , A >.