Step |
Hyp |
Ref |
Expression |
1 |
|
op2ndg |
|- ( ( A e. V /\ B e. W ) -> ( 2nd ` <. A , B >. ) = B ) |
2 |
1
|
eqeq1d |
|- ( ( A e. V /\ B e. W ) -> ( ( 2nd ` <. A , B >. ) = C <-> B = C ) ) |
3 |
|
fo2nd |
|- 2nd : _V -onto-> _V |
4 |
|
fofn |
|- ( 2nd : _V -onto-> _V -> 2nd Fn _V ) |
5 |
3 4
|
ax-mp |
|- 2nd Fn _V |
6 |
|
opex |
|- <. A , B >. e. _V |
7 |
|
fnbrfvb |
|- ( ( 2nd Fn _V /\ <. A , B >. e. _V ) -> ( ( 2nd ` <. A , B >. ) = C <-> <. A , B >. 2nd C ) ) |
8 |
5 6 7
|
mp2an |
|- ( ( 2nd ` <. A , B >. ) = C <-> <. A , B >. 2nd C ) |
9 |
|
eqcom |
|- ( B = C <-> C = B ) |
10 |
2 8 9
|
3bitr3g |
|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. 2nd C <-> C = B ) ) |