Step |
Hyp |
Ref |
Expression |
1 |
|
opex |
|- <. A , B >. e. _V |
2 |
|
setsvalg |
|- ( ( S e. V /\ <. A , B >. e. _V ) -> ( S sSet <. A , B >. ) = ( ( S |` ( _V \ dom { <. A , B >. } ) ) u. { <. A , B >. } ) ) |
3 |
1 2
|
mpan2 |
|- ( S e. V -> ( S sSet <. A , B >. ) = ( ( S |` ( _V \ dom { <. A , B >. } ) ) u. { <. A , B >. } ) ) |
4 |
|
dmsnopg |
|- ( B e. W -> dom { <. A , B >. } = { A } ) |
5 |
4
|
difeq2d |
|- ( B e. W -> ( _V \ dom { <. A , B >. } ) = ( _V \ { A } ) ) |
6 |
5
|
reseq2d |
|- ( B e. W -> ( S |` ( _V \ dom { <. A , B >. } ) ) = ( S |` ( _V \ { A } ) ) ) |
7 |
6
|
uneq1d |
|- ( B e. W -> ( ( S |` ( _V \ dom { <. A , B >. } ) ) u. { <. A , B >. } ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , B >. } ) ) |
8 |
3 7
|
sylan9eq |
|- ( ( S e. V /\ B e. W ) -> ( S sSet <. A , B >. ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , B >. } ) ) |