Metamath Proof Explorer

Theorem setsabs

Description: Replacing the same components twice yields the same as the second setting only. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Assertion setsabs 
|- ( ( S e. V /\ C e. W ) -> ( ( S sSet <. A , B >. ) sSet <. A , C >. ) = ( S sSet <. A , C >. ) )

Proof

Step Hyp Ref Expression
1 setsres 
 |-  ( S e. V -> ( ( S sSet <. A , B >. ) |` ( _V \ { A } ) ) = ( S |` ( _V \ { A } ) ) )
2 1 adantr 
 |-  ( ( S e. V /\ C e. W ) -> ( ( S sSet <. A , B >. ) |` ( _V \ { A } ) ) = ( S |` ( _V \ { A } ) ) )
3 2 uneq1d 
 |-  ( ( S e. V /\ C e. W ) -> ( ( ( S sSet <. A , B >. ) |` ( _V \ { A } ) ) u. { <. A , C >. } ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , C >. } ) )
4 ovexd 
 |-  ( S e. V -> ( S sSet <. A , B >. ) e. _V )
5 setsval 
 |-  ( ( ( S sSet <. A , B >. ) e. _V /\ C e. W ) -> ( ( S sSet <. A , B >. ) sSet <. A , C >. ) = ( ( ( S sSet <. A , B >. ) |` ( _V \ { A } ) ) u. { <. A , C >. } ) )
6 4 5 sylan 
 |-  ( ( S e. V /\ C e. W ) -> ( ( S sSet <. A , B >. ) sSet <. A , C >. ) = ( ( ( S sSet <. A , B >. ) |` ( _V \ { A } ) ) u. { <. A , C >. } ) )
7 setsval 
 |-  ( ( S e. V /\ C e. W ) -> ( S sSet <. A , C >. ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , C >. } ) )
8 3 6 7 3eqtr4d 
 |-  ( ( S e. V /\ C e. W ) -> ( ( S sSet <. A , B >. ) sSet <. A , C >. ) = ( S sSet <. A , C >. ) )