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

Metamath Proof Explorer

Theorem fvpr2g

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

Ref Expression
Assertion fvpr2g 
|- ( ( 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 1 fveq1i 
 |-  ( { <. A , C >. , <. B , D >. } ` B ) = ( { <. B , D >. , <. A , C >. } ` B )
3 necom 
 |-  ( A =/= B <-> B =/= A )
4 fvpr1g 
 |-  ( ( B e. V /\ D e. W /\ B =/= A ) -> ( { <. B , D >. , <. A , C >. } ` B ) = D )
5 3 4 syl3an3b 
 |-  ( ( B e. V /\ D e. W /\ A =/= B ) -> ( { <. B , D >. , <. A , C >. } ` B ) = D )
6 2 5 eqtrid 
 |-  ( ( B e. V /\ D e. W /\ A =/= B ) -> ( { <. A , C >. , <. B , D >. } ` B ) = D )