Theorem fvpr2gOLD

Description: Obsolete version of fvpr2g as of 26-Sep-2024. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		prcom	|- { <. A , C >. , <. B , D >. } = { <. B , D >. , <. A , C >. }
2		df-pr	|- { <. B , D >. , <. A , C >. } = ( { <. B , D >. } u. { <. A , C >. } )
3	1 2	eqtri	|- { <. A , C >. , <. B , D >. } = ( { <. B , D >. } u. { <. A , C >. } )
4	3	fveq1i	|- ( { <. A , C >. , <. B , D >. } ` B ) = ( ( { <. B , D >. } u. { <. A , C >. } ) ` B )
5		fvunsn	|- ( A =/= B -> ( ( { <. B , D >. } u. { <. A , C >. } ) ` B ) = ( { <. B , D >. } ` B ) )
6	4 5	eqtrid	|- ( A =/= B -> ( { <. A , C >. , <. B , D >. } ` B ) = ( { <. B , D >. } ` B ) )
7	6	3ad2ant3	|- ( ( B e. V /\ D e. W /\ A =/= B ) -> ( { <. A , C >. , <. B , D >. } ` B ) = ( { <. B , D >. } ` B ) )
8		fvsng	|- ( ( B e. V /\ D e. W ) -> ( { <. B , D >. } ` B ) = D )
9	8	3adant3	|- ( ( B e. V /\ D e. W /\ A =/= B ) -> ( { <. B , D >. } ` B ) = D )
10	7 9	eqtrd	|- ( ( B e. V /\ D e. W /\ A =/= B ) -> ( { <. A , C >. , <. B , D >. } ` B ) = D )