Theorem bj-fvsnun1

Description: The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. (Contributed by NM, 23-Sep-2007) Put in deduction form and remove two sethood hypotheses. (Revised by BJ, 18-Mar-2023)

	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-fvsnun1.eldif	$$⊢\phi \to D\in \left(C\setminus \left\{A\right\}\right)$$
Assertion	bj-fvsnun1	$$⊢\phi \to G\left(D\right)=F\left(D\right)$$

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-fvsnun1.eldif	$$⊢\phi \to D\in \left(C\setminus \left\{A\right\}\right)$$
3		eldifsnneq	$$⊢D\in \left(C\setminus \left\{A\right\}\right)\to \neg D=A$$
4	2 3	syl	$$⊢\phi \to \neg D=A$$
5	1 4	bj-fununsn1	$$⊢\phi \to G\left(D\right)=\left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\left(D\right)$$
6	2	fvresd	$$⊢\phi \to \left({F\upharpoonright }_{\left(C\setminus \left\{A\right\}\right)}\right)\left(D\right)=F\left(D\right)$$
7	5 6	eqtrd	$$⊢\phi \to G\left(D\right)=F\left(D\right)$$