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

Metamath Proof Explorer

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 )