Theorem bj-fvsnun2

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, 18-Mar-2023) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-fvsnun.un	$$⊢\phi \to G=\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}$$
	bj-fvsnun2.ex1	$$⊢\phi \to A\in V$$
	bj-fvsnun2.ex2	$$⊢\phi \to B\in W$$
Assertion	bj-fvsnun2	$$⊢\phi \to G\left(A\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		bj-fvsnun.un	$$⊢\phi \to G=\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\cup \left\{⟨A,B⟩\right\}$$
2		bj-fvsnun2.ex1	$$⊢\phi \to A\in V$$
3		bj-fvsnun2.ex2	$$⊢\phi \to B\in W$$
4		dmres	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)=\left(C\setminus \left\{A\right\}\right)\cap \mathrm{dom}F$$
5		inss1	$$⊢\left(C\setminus \left\{A\right\}\right)\cap \mathrm{dom}F\subseteq C\setminus \left\{A\right\}$$
6	4 5	eqsstri	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\subseteq C\setminus \left\{A\right\}$$
7	6	a1i	$$⊢\phi \to \mathrm{dom}\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\subseteq C\setminus \left\{A\right\}$$
8		neldifsnd	$$⊢\phi \to \neg A\in \left(C\setminus \left\{A\right\}\right)$$
9	7 8	ssneldd	$$⊢\phi \to \neg A\in \mathrm{dom}\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)$$
10	1 9 2 3	bj-fununsn2	$$⊢\phi \to G\left(A\right)=B$$