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 } ) ) )`
` |-  ( ( S e. V /\ C e. W ) -> ( ( S sSet <. A , B >. ) |` ( _V \ { A } ) ) = ( S |` ( _V \ { A } ) ) )`
` |-  ( ( S e. V /\ C e. W ) -> ( ( ( S sSet <. A , B >. ) |` ( _V \ { A } ) ) u. { <. A , C >. } ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , C >. } ) )`
` |-  ( S e. V -> ( S sSet <. A , B >. ) e. _V )`
` |-  ( ( ( 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 >. } ) )`
` |-  ( ( S e. V /\ C e. W ) -> ( ( S sSet <. A , B >. ) sSet <. A , C >. ) = ( ( ( S sSet <. A , B >. ) |` ( _V \ { A } ) ) u. { <. A , C >. } ) )`
` |-  ( ( S e. V /\ C e. W ) -> ( S sSet <. A , C >. ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , C >. } ) )`
` |-  ( ( S e. V /\ C e. W ) -> ( ( S sSet <. A , B >. ) sSet <. A , C >. ) = ( S sSet <. A , C >. ) )`