This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rnpropg

Description: The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017)

Ref Expression
Assertion rnpropg 
|- ( ( A e. V /\ B e. W ) -> ran { <. A , C >. , <. B , D >. } = { C , D } )

Proof

Step Hyp Ref Expression
1 df-pr 
 |-  { <. A , C >. , <. B , D >. } = ( { <. A , C >. } u. { <. B , D >. } )
2 1 rneqi 
 |-  ran { <. A , C >. , <. B , D >. } = ran ( { <. A , C >. } u. { <. B , D >. } )
3 rnsnopg 
 |-  ( A e. V -> ran { <. A , C >. } = { C } )
4 3 adantr 
 |-  ( ( A e. V /\ B e. W ) -> ran { <. A , C >. } = { C } )
5 rnsnopg 
 |-  ( B e. W -> ran { <. B , D >. } = { D } )
6 5 adantl 
 |-  ( ( A e. V /\ B e. W ) -> ran { <. B , D >. } = { D } )
7 4 6 uneq12d 
 |-  ( ( A e. V /\ B e. W ) -> ( ran { <. A , C >. } u. ran { <. B , D >. } ) = ( { C } u. { D } ) )
8 rnun 
 |-  ran ( { <. A , C >. } u. { <. B , D >. } ) = ( ran { <. A , C >. } u. ran { <. B , D >. } )
9 df-pr 
 |-  { C , D } = ( { C } u. { D } )
10 7 8 9 3eqtr4g 
 |-  ( ( A e. V /\ B e. W ) -> ran ( { <. A , C >. } u. { <. B , D >. } ) = { C , D } )
11 2 10 eqtrid 
 |-  ( ( A e. V /\ B e. W ) -> ran { <. A , C >. , <. B , D >. } = { C , D } )