Metamath Proof Explorer

Theorem fvtp2

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

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

Proof

Step Hyp Ref Expression
1 fvtp2.1 
 |-  B e. _V
2 fvtp2.4 
 |-  E e. _V
3 tprot 
 |-  { <. A , D >. , <. B , E >. , <. C , F >. } = { <. B , E >. , <. C , F >. , <. A , D >. }
4 3 fveq1i 
 |-  ( { <. A , D >. , <. B , E >. , <. C , F >. } ` B ) = ( { <. B , E >. , <. C , F >. , <. A , D >. } ` B )
5 necom 
 |-  ( A =/= B <-> B =/= A )
6 1 2 fvtp1 
 |-  ( ( B =/= C /\ B =/= A ) -> ( { <. B , E >. , <. C , F >. , <. A , D >. } ` B ) = E )
7 6 ancoms 
 |-  ( ( B =/= A /\ B =/= C ) -> ( { <. B , E >. , <. C , F >. , <. A , D >. } ` B ) = E )
8 5 7 sylanb 
 |-  ( ( A =/= B /\ B =/= C ) -> ( { <. B , E >. , <. C , F >. , <. A , D >. } ` B ) = E )
9 4 8 syl5eq 
 |-  ( ( A =/= B /\ B =/= C ) -> ( { <. A , D >. , <. B , E >. , <. C , F >. } ` B ) = E )