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