Metamath Proof Explorer

Theorem 2nd1st

Description: Swap the members of an ordered pair. (Contributed by NM, 31-Dec-2014)

Ref Expression
Assertion 2nd1st 
|- ( A e. ( B X. C ) -> U. `' { A } = <. ( 2nd ` A ) , ( 1st ` A ) >. )

Proof

Step Hyp Ref Expression
1 1st2nd2 
 |-  ( A e. ( B X. C ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
2 1 sneqd 
 |-  ( A e. ( B X. C ) -> { A } = { <. ( 1st ` A ) , ( 2nd ` A ) >. } )
3 2 cnveqd 
 |-  ( A e. ( B X. C ) -> `' { A } = `' { <. ( 1st ` A ) , ( 2nd ` A ) >. } )
4 3 unieqd 
 |-  ( A e. ( B X. C ) -> U. `' { A } = U. `' { <. ( 1st ` A ) , ( 2nd ` A ) >. } )
5 opswap 
 |-  U. `' { <. ( 1st ` A ) , ( 2nd ` A ) >. } = <. ( 2nd ` A ) , ( 1st ` A ) >.
6 4 5 eqtrdi 
 |-  ( A e. ( B X. C ) -> U. `' { A } = <. ( 2nd ` A ) , ( 1st ` A ) >. )