Theorem setsidel

Description: The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021)

	Ref	Expression
Hypotheses	setsidel.s	|- ( ph -> S e. V )
	setsidel.b	|- ( ph -> B e. W )
	setsidel.r	|- R = ( S sSet <. A , B >. )
Assertion	setsidel	|- ( ph -> <. A , B >. e. R )

Proof

Step	Hyp	Ref	Expression
1		setsidel.s	|- ( ph -> S e. V )
2		setsidel.b	|- ( ph -> B e. W )
3		setsidel.r	|- R = ( S sSet <. A , B >. )
4		opex	|- <. A , B >. e. _V
5	4	snid	|- <. A , B >. e. { <. A , B >. }
6		elun2	|- ( <. A , B >. e. { <. A , B >. } -> <. A , B >. e. ( ( S |` ( _V \ { A } ) ) u. { <. A , B >. } ) )
7	5 6	mp1i	|- ( ph -> <. A , B >. e. ( ( S |` ( _V \ { A } ) ) u. { <. A , B >. } ) )
8		setsval	|- ( ( S e. V /\ B e. W ) -> ( S sSet <. A , B >. ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , B >. } ) )
9	1 2 8	syl2anc	|- ( ph -> ( S sSet <. A , B >. ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , B >. } ) )
10	3 9	eqtrid	|- ( ph -> R = ( ( S |` ( _V \ { A } ) ) u. { <. A , B >. } ) )
11	7 10	eleqtrrd	|- ( ph -> <. A , B >. e. R )