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