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	$$⊢\left(S\in V\wedge C\in W\right)\to \left(S\mathrm{sSet}⟨A,B⟩\right)\mathrm{sSet}⟨A,C⟩=S\mathrm{sSet}⟨A,C⟩$$

Proof

Step	Hyp	Ref	Expression
1		setsres	$$⊢S\in V\to {\left(S\mathrm{sSet}⟨A,B⟩\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}={S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}$$
2	1	adantr	$$⊢\left(S\in V\wedge C\in W\right)\to {\left(S\mathrm{sSet}⟨A,B⟩\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}={S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}$$
3	2	uneq1d	$$⊢\left(S\in V\wedge C\in W\right)\to \left({\left(S\mathrm{sSet}⟨A,B⟩\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,C⟩\right\}=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,C⟩\right\}$$
4		ovexd	$$⊢S\in V\to S\mathrm{sSet}⟨A,B⟩\in \mathrm{V}$$
5		setsval	$$⊢\left(S\mathrm{sSet}⟨A,B⟩\in \mathrm{V}\wedge C\in W\right)\to \left(S\mathrm{sSet}⟨A,B⟩\right)\mathrm{sSet}⟨A,C⟩=\left({\left(S\mathrm{sSet}⟨A,B⟩\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,C⟩\right\}$$
6	4 5	sylan	$$⊢\left(S\in V\wedge C\in W\right)\to \left(S\mathrm{sSet}⟨A,B⟩\right)\mathrm{sSet}⟨A,C⟩=\left({\left(S\mathrm{sSet}⟨A,B⟩\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,C⟩\right\}$$
7		setsval	$$⊢\left(S\in V\wedge C\in W\right)\to S\mathrm{sSet}⟨A,C⟩=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,C⟩\right\}$$
8	3 6 7	3eqtr4d	$$⊢\left(S\in V\wedge C\in W\right)\to \left(S\mathrm{sSet}⟨A,B⟩\right)\mathrm{sSet}⟨A,C⟩=S\mathrm{sSet}⟨A,C⟩$$