Theorem fvsnun1

Description: The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 . (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)$$
Assertion	fvsnun1	$$⊢\phi \to G\left(A\right)=B$$

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	3	reseq1i	$$⊢{G\upharpoonright }_{\left\{A\right\}}={\left(\left\{⟨A,B⟩\right\}\cup \left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\right)\upharpoonright }_{\left\{A\right\}}$$
5		resundir	$$⊢{\left(\left\{⟨A,B⟩\right\}\cup \left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\right)\upharpoonright }_{\left\{A\right\}}=\left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left\{A\right\}}\right)\cup \left({\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\upharpoonright }_{\left\{A\right\}}\right)$$
6		disjdifr	$$⊢\left(C\setminus \left\{A\right\}\right)\cap \left\{A\right\}=\varnothing$$
7		resdisj	$$⊢\left(C\setminus \left\{A\right\}\right)\cap \left\{A\right\}=\varnothing \to {\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\upharpoonright }_{\left\{A\right\}}=\varnothing$$
8	6 7	ax-mp	$$⊢{\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\upharpoonright }_{\left\{A\right\}}=\varnothing$$
9	8	uneq2i	$$⊢\left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left\{A\right\}}\right)\cup \left({\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\upharpoonright }_{\left\{A\right\}}\right)=\left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left\{A\right\}}\right)\cup \varnothing$$
10		un0	$$⊢\left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left\{A\right\}}\right)\cup \varnothing ={\left\{⟨A,B⟩\right\}\upharpoonright }_{\left\{A\right\}}$$
11	9 10	eqtri	$$⊢\left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left\{A\right\}}\right)\cup \left({\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\upharpoonright }_{\left\{A\right\}}\right)={\left\{⟨A,B⟩\right\}\upharpoonright }_{\left\{A\right\}}$$
12	5 11	eqtri	$$⊢{\left(\left\{⟨A,B⟩\right\}\cup \left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\right)\upharpoonright }_{\left\{A\right\}}={\left\{⟨A,B⟩\right\}\upharpoonright }_{\left\{A\right\}}$$
13	4 12	eqtri	$$⊢{G\upharpoonright }_{\left\{A\right\}}={\left\{⟨A,B⟩\right\}\upharpoonright }_{\left\{A\right\}}$$
14	13	fveq1i	$$⊢\left({G\upharpoonright }_{\left\{A\right\}}\right)\left(A\right)=\left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left\{A\right\}}\right)\left(A\right)$$
15		snidg	$$⊢A\in V\to A\in \left\{A\right\}$$
16	1 15	syl	$$⊢\phi \to A\in \left\{A\right\}$$
17	16	fvresd	$$⊢\phi \to \left({G\upharpoonright }_{\left\{A\right\}}\right)\left(A\right)=G\left(A\right)$$
18	16	fvresd	$$⊢\phi \to \left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left\{A\right\}}\right)\left(A\right)=\left\{⟨A,B⟩\right\}\left(A\right)$$
19		fvsng	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{⟨A,B⟩\right\}\left(A\right)=B$$
20	1 2 19	syl2anc	$$⊢\phi \to \left\{⟨A,B⟩\right\}\left(A\right)=B$$
21	18 20	eqtrd	$$⊢\phi \to \left({\left\{⟨A,B⟩\right\}\upharpoonright }_{\left\{A\right\}}\right)\left(A\right)=B$$
22	14 17 21	3eqtr3a	$$⊢\phi \to G\left(A\right)=B$$