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	syl5eq	|- ( ( A e. V /\ B e. W ) -> ran { <. A , C >. , <. B , D >. } = { C , D } )