Theorem setsnidel

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 >. )
	setsnidel.c	|- ( ph -> C e. X )
	setsnidel.d	|- ( ph -> D e. Y )
	setsnidel.s	|- ( ph -> <. C , D >. e. S )
	setsnidel.n	|- ( ph -> A =/= C )
Assertion	setsnidel	|- ( ph -> <. C , D >. 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		setsnidel.c	|- ( ph -> C e. X )
5		setsnidel.d	|- ( ph -> D e. Y )
6		setsnidel.s	|- ( ph -> <. C , D >. e. S )
7		setsnidel.n	|- ( ph -> A =/= C )
8	4	elexd	|- ( ph -> C e. _V )
9	7	necomd	|- ( ph -> C =/= A )
10		eldifsn	|- ( C e. ( _V \ { A } ) <-> ( C e. _V /\ C =/= A ) )
11	8 9 10	sylanbrc	|- ( ph -> C e. ( _V \ { A } ) )
12		opelres	|- ( D e. Y -> ( <. C , D >. e. ( S |` ( _V \ { A } ) ) <-> ( C e. ( _V \ { A } ) /\ <. C , D >. e. S ) ) )
13	5 12	syl	|- ( ph -> ( <. C , D >. e. ( S |` ( _V \ { A } ) ) <-> ( C e. ( _V \ { A } ) /\ <. C , D >. e. S ) ) )
14	11 6 13	mpbir2and	|- ( ph -> <. C , D >. e. ( S |` ( _V \ { A } ) ) )
15		elun1	|- ( <. C , D >. e. ( S |` ( _V \ { A } ) ) -> <. C , D >. e. ( ( S |` ( _V \ { A } ) ) u. { <. A , B >. } ) )
16	14 15	syl	|- ( ph -> <. C , D >. e. ( ( S |` ( _V \ { A } ) ) u. { <. A , B >. } ) )
17		setsval	|- ( ( S e. V /\ B e. W ) -> ( S sSet <. A , B >. ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , B >. } ) )
18	1 2 17	syl2anc	|- ( ph -> ( S sSet <. A , B >. ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , B >. } ) )
19	3 18	syl5eq	|- ( ph -> R = ( ( S |` ( _V \ { A } ) ) u. { <. A , B >. } ) )
20	16 19	eleqtrrd	|- ( ph -> <. C , D >. e. R )