Theorem setsval

Description: Value of the structure replacement function. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Assertion	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\}$$

Proof

Step	Hyp	Ref	Expression
1		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
2		setsvalg	$$⊢\left(S\in V\wedge ⟨A,B⟩\in \mathrm{V}\right)\to S\mathrm{sSet}⟨A,B⟩=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}$$
3	1 2	mpan2	$$⊢S\in V\to S\mathrm{sSet}⟨A,B⟩=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}$$
4		dmsnopg	$$⊢B\in W\to \mathrm{dom}\left\{⟨A,B⟩\right\}=\left\{A\right\}$$
5	4	difeq2d	$$⊢B\in W\to \mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}=\mathrm{V}\setminus \left\{A\right\}$$
6	5	reseq2d	$$⊢B\in W\to {S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}\right)}={S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}$$
7	6	uneq1d	$$⊢B\in W\to \left({S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{⟨A,B⟩\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}$$
8	3 7	sylan9eq	$$⊢\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\}$$