Theorem fvpr1g

Description: The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017)

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

Proof

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