Theorem fvsnun2

Description: The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. See also fvsnun1 . (Contributed by NM, 23-Sep-2007) Put in deduction form. (Revised by BJ, 25-Feb-2023)

	Ref	Expression
Hypotheses	fvsnun.1	$$⊢\phi \to A\in V$$
	fvsnun.2	$$⊢\phi \to B\in W$$
	fvsnun.3	$$⊢G=\left\{⟨A,B⟩\right\}\cup \left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)$$
	fvsnun2.4	$$⊢\phi \to D\in \left(C\setminus \left\{A\right\}\right)$$
Assertion	fvsnun2	$$⊢\phi \to G\left(D\right)=F\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvsnun.1	$$⊢\phi \to A\in V$$
2		fvsnun.2	$$⊢\phi \to B\in W$$
3		fvsnun.3	$$⊢G=\left\{⟨A,B⟩\right\}\cup \left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)$$
4		fvsnun2.4	$$⊢\phi \to D\in \left(C\setminus \left\{A\right\}\right)$$
5	3	reseq1i	$$⊢{G\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}={\left(\left\{⟨A,B⟩\right\}\cup \left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\right)\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}$$
6	5	a1i	$$⊢\phi \to {G\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}={\left(\left\{⟨A,B⟩\right\}\cup \left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\right)\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}$$
7		resundir	$$⊢{\left(\left\{⟨A,B⟩\right\}\cup \left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\right)\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}=\left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\cup \left({\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)$$
8	7	a1i	$$⊢\phi \to {\left(\left\{⟨A,B⟩\right\}\cup \left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\right)\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}=\left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\cup \left({\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)$$
9		disjdif	$$⊢\left\{A\right\}\cap \left(C\setminus \left\{A\right\}\right)=\varnothing$$
10		fnsng	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{⟨A,B⟩\right\}Fn\left\{A\right\}$$
11	1 2 10	syl2anc	$$⊢\phi \to \left\{⟨A,B⟩\right\}Fn\left\{A\right\}$$
12		fnresdisj	$$⊢\left\{⟨A,B⟩\right\}Fn\left\{A\right\}\to \left(\left\{A\right\}\cap \left(C\setminus \left\{A\right\}\right)=\varnothing \leftrightarrow {\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}=\varnothing \right)$$
13	11 12	syl	$$⊢\phi \to \left(\left\{A\right\}\cap \left(C\setminus \left\{A\right\}\right)=\varnothing \leftrightarrow {\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}=\varnothing \right)$$
14	9 13	mpbii	$$⊢\phi \to {\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}=\varnothing$$
15		residm	$$⊢{\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}={F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}$$
16	15	a1i	$$⊢\phi \to {\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}={F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}$$
17	14 16	uneq12d	$$⊢\phi \to \left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\cup \left({\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)=\varnothing \cup \left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)$$
18		uncom	$$⊢\varnothing \cup \left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)=\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\cup \varnothing$$
19	18	a1i	$$⊢\phi \to \varnothing \cup \left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)=\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\cup \varnothing$$
20		un0	$$⊢\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\cup \varnothing ={F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}$$
21	20	a1i	$$⊢\phi \to \left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\cup \varnothing ={F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}$$
22	17 19 21	3eqtrd	$$⊢\phi \to \left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\cup \left({\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)={F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}$$
23	6 8 22	3eqtrd	$$⊢\phi \to {G\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}={F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}$$
24	23	fveq1d	$$⊢\phi \to \left({G\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\left(D\right)=\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\left(D\right)$$
25	4	fvresd	$$⊢\phi \to \left({G\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\left(D\right)=G\left(D\right)$$
26	4	fvresd	$$⊢\phi \to \left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\left(D\right)=F\left(D\right)$$
27	24 25 26	3eqtr3d	$$⊢\phi \to G\left(D\right)=F\left(D\right)$$