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

Metamath Proof Explorer

Theorem fvtp1

Description: The first value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011)

Ref Expression
Hypotheses fvtp1.1 
|- A e. _V
fvtp1.4 
|- D e. _V
Assertion fvtp1 
|- ( ( A =/= B /\ A =/= C ) -> ( { <. A , D >. , <. B , E >. , <. C , F >. } ` A ) = D )

Proof

Step Hyp Ref Expression
1 fvtp1.1 
 |-  A e. _V
2 fvtp1.4 
 |-  D e. _V
3 df-tp 
 |-  { <. A , D >. , <. B , E >. , <. C , F >. } = ( { <. A , D >. , <. B , E >. } u. { <. C , F >. } )
4 3 fveq1i 
 |-  ( { <. A , D >. , <. B , E >. , <. C , F >. } ` A ) = ( ( { <. A , D >. , <. B , E >. } u. { <. C , F >. } ) ` A )
5 necom 
 |-  ( A =/= C <-> C =/= A )
6 fvunsn 
 |-  ( C =/= A -> ( ( { <. A , D >. , <. B , E >. } u. { <. C , F >. } ) ` A ) = ( { <. A , D >. , <. B , E >. } ` A ) )
7 5 6 sylbi 
 |-  ( A =/= C -> ( ( { <. A , D >. , <. B , E >. } u. { <. C , F >. } ) ` A ) = ( { <. A , D >. , <. B , E >. } ` A ) )
8 1 2 fvpr1 
 |-  ( A =/= B -> ( { <. A , D >. , <. B , E >. } ` A ) = D )
9 7 8 sylan9eqr 
 |-  ( ( A =/= B /\ A =/= C ) -> ( ( { <. A , D >. , <. B , E >. } u. { <. C , F >. } ) ` A ) = D )
10 4 9 eqtrid 
 |-  ( ( A =/= B /\ A =/= C ) -> ( { <. A , D >. , <. B , E >. , <. C , F >. } ` A ) = D )