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
|
syl5eq |
|- ( ( B e. V /\ D e. W /\ A =/= B ) -> ( { <. A , C >. , <. B , D >. } ` B ) = D ) |