Theorem fvunsn

Description: Remove an ordered pair not participating in a function value. (Contributed by NM, 1-Oct-2013) (Revised by Mario Carneiro, 28-May-2014)

	Ref	Expression
Assertion	fvunsn	$$⊢B\ne D\to \left(A\cup \left\{⟨B,C⟩\right\}\right)\left(D\right)=A\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		resundir	$$⊢{\left(A\cup \left\{⟨B,C⟩\right\}\right)\upharpoonright }_{\left\{D\right\}}=\left({A\upharpoonright }_{\left\{D\right\}}\right)\cup \left({\left\{⟨B,C⟩\right\}\upharpoonright }_{\left\{D\right\}}\right)$$
2		nelsn	$$⊢B\ne D\to \neg B\in \left\{D\right\}$$
3		ressnop0	$$⊢\neg B\in \left\{D\right\}\to {\left\{⟨B,C⟩\right\}\upharpoonright }_{\left\{D\right\}}=\varnothing$$
4	2 3	syl	$$⊢B\ne D\to {\left\{⟨B,C⟩\right\}\upharpoonright }_{\left\{D\right\}}=\varnothing$$
5	4	uneq2d	$$⊢B\ne D\to \left({A\upharpoonright }_{\left\{D\right\}}\right)\cup \left({\left\{⟨B,C⟩\right\}\upharpoonright }_{\left\{D\right\}}\right)=\left({A\upharpoonright }_{\left\{D\right\}}\right)\cup \varnothing$$
6		un0	$$⊢\left({A\upharpoonright }_{\left\{D\right\}}\right)\cup \varnothing ={A\upharpoonright }_{\left\{D\right\}}$$
7	5 6	eqtrdi	$$⊢B\ne D\to \left({A\upharpoonright }_{\left\{D\right\}}\right)\cup \left({\left\{⟨B,C⟩\right\}\upharpoonright }_{\left\{D\right\}}\right)={A\upharpoonright }_{\left\{D\right\}}$$
8	1 7	syl5eq	$$⊢B\ne D\to {\left(A\cup \left\{⟨B,C⟩\right\}\right)\upharpoonright }_{\left\{D\right\}}={A\upharpoonright }_{\left\{D\right\}}$$
9	8	fveq1d	$$⊢B\ne D\to \left({\left(A\cup \left\{⟨B,C⟩\right\}\right)\upharpoonright }_{\left\{D\right\}}\right)\left(D\right)=\left({A\upharpoonright }_{\left\{D\right\}}\right)\left(D\right)$$
10		fvressn	$$⊢D\in \mathrm{V}\to \left({\left(A\cup \left\{⟨B,C⟩\right\}\right)\upharpoonright }_{\left\{D\right\}}\right)\left(D\right)=\left(A\cup \left\{⟨B,C⟩\right\}\right)\left(D\right)$$
11		fvprc	$$⊢\neg D\in \mathrm{V}\to \left({\left(A\cup \left\{⟨B,C⟩\right\}\right)\upharpoonright }_{\left\{D\right\}}\right)\left(D\right)=\varnothing$$
12		fvprc	$$⊢\neg D\in \mathrm{V}\to \left(A\cup \left\{⟨B,C⟩\right\}\right)\left(D\right)=\varnothing$$
13	11 12	eqtr4d	$$⊢\neg D\in \mathrm{V}\to \left({\left(A\cup \left\{⟨B,C⟩\right\}\right)\upharpoonright }_{\left\{D\right\}}\right)\left(D\right)=\left(A\cup \left\{⟨B,C⟩\right\}\right)\left(D\right)$$
14	10 13	pm2.61i	$$⊢\left({\left(A\cup \left\{⟨B,C⟩\right\}\right)\upharpoonright }_{\left\{D\right\}}\right)\left(D\right)=\left(A\cup \left\{⟨B,C⟩\right\}\right)\left(D\right)$$
15		fvressn	$$⊢D\in \mathrm{V}\to \left({A\upharpoonright }_{\left\{D\right\}}\right)\left(D\right)=A\left(D\right)$$
16		fvprc	$$⊢\neg D\in \mathrm{V}\to \left({A\upharpoonright }_{\left\{D\right\}}\right)\left(D\right)=\varnothing$$
17		fvprc	$$⊢\neg D\in \mathrm{V}\to A\left(D\right)=\varnothing$$
18	16 17	eqtr4d	$$⊢\neg D\in \mathrm{V}\to \left({A\upharpoonright }_{\left\{D\right\}}\right)\left(D\right)=A\left(D\right)$$
19	15 18	pm2.61i	$$⊢\left({A\upharpoonright }_{\left\{D\right\}}\right)\left(D\right)=A\left(D\right)$$
20	9 14 19	3eqtr3g	$$⊢B\ne D\to \left(A\cup \left\{⟨B,C⟩\right\}\right)\left(D\right)=A\left(D\right)$$