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	$$⊢\phi \to S\in V$$
	setsidel.b	$$⊢\phi \to B\in W$$
	setsidel.r	$$⊢R=S\mathrm{sSet}⟨A,B⟩$$
Assertion	setsidel	$$⊢\phi \to ⟨A,B⟩\in R$$

Proof

Step	Hyp	Ref	Expression
1		setsidel.s	$$⊢\phi \to S\in V$$
2		setsidel.b	$$⊢\phi \to B\in W$$
3		setsidel.r	$$⊢R=S\mathrm{sSet}⟨A,B⟩$$
4		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
5	4	snid	$$⊢⟨A,B⟩\in \left\{⟨A,B⟩\right\}$$
6		elun2	$$⊢⟨A,B⟩\in \left\{⟨A,B⟩\right\}\to ⟨A,B⟩\in \left(\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}\right)$$
7	5 6	mp1i	$$⊢\phi \to ⟨A,B⟩\in \left(\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}\right)$$
8		setsval	$$⊢\left(S\in V\wedge B\in W\right)\to S\mathrm{sSet}⟨A,B⟩=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}$$
9	1 2 8	syl2anc	$$⊢\phi \to S\mathrm{sSet}⟨A,B⟩=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}$$
10	3 9	syl5eq	$$⊢\phi \to R=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}$$
11	7 10	eleqtrrd	$$⊢\phi \to ⟨A,B⟩\in R$$