Step |
Hyp |
Ref |
Expression |
1 |
|
xpss |
|- ( V X. W ) C_ ( _V X. _V ) |
2 |
1
|
sseli |
|- ( A e. ( V X. W ) -> A e. ( _V X. _V ) ) |
3 |
|
elxp6 |
|- ( A e. ( _V X. _V ) <-> ( A = <. ( 1st ` A ) , ( 2nd ` A ) >. /\ ( ( 1st ` A ) e. _V /\ ( 2nd ` A ) e. _V ) ) ) |
4 |
3
|
simplbi |
|- ( A e. ( _V X. _V ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. ) |
5 |
|
opeq12 |
|- ( ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) -> <. ( 1st ` A ) , ( 2nd ` A ) >. = <. B , C >. ) |
6 |
4 5
|
sylan9eq |
|- ( ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) ) -> A = <. B , C >. ) |
7 |
2 6
|
sylan |
|- ( ( A e. ( V X. W ) /\ ( ( 1st ` A ) = B /\ ( 2nd ` A ) = C ) ) -> A = <. B , C >. ) |