Metamath Proof Explorer

Theorem setsstrset

Description: Relation between df-sets and df-strset . Temporary theorem kept during the transition from the former to the latter. (Contributed by BJ, 13-Feb-2022)

		Ref	Expression
	Assertion	setsstrset	\|- ( ( S e. V /\ B e. W ) -> [s B / A ]s S = ( S sSet <. ( A ` ndx ) , B >. ) )

Proof

Step	Hyp	Ref	Expression
1		df-strset	\|- [s B / A ]s S = ( ( S \|` ( _V \ { ( A ` ndx ) } ) ) u. { <. ( A ` ndx ) , B >. } )
2		setsval	\|- ( ( S e. V /\ B e. W ) -> ( S sSet <. ( A ` ndx ) , B >. ) = ( ( S \|` ( _V \ { ( A ` ndx ) } ) ) u. { <. ( A ` ndx ) , B >. } ) )
3	1 2	eqtr4id	\|- ( ( S e. V /\ B e. W ) -> [s B / A ]s S = ( S sSet <. ( A ` ndx ) , B >. ) )

Step

Hyp

Ref

Expression

df-strset

 |-  [s B / A ]s S = ( ( S |` ( _V \ { ( A ` ndx ) } ) ) u. { <. ( A ` ndx ) , B >. } )

setsval

 |-  ( ( S e. V /\ B e. W ) -> ( S sSet <. ( A ` ndx ) , B >. ) = ( ( S |` ( _V \ { ( A ` ndx ) } ) ) u. { <. ( A ` ndx ) , B >. } ) )

1 2

eqtr4id

 |-  ( ( S e. V /\ B e. W ) -> [s B / A ]s S = ( S sSet <. ( A ` ndx ) , B >. ) )