Theorem fmptunsnop

Description: Two ways to express a function with a value replaced. (Contributed by Thierry Arnoux, 5-Oct-2025)

	Ref	Expression
Hypotheses	fmptunsnop.1	$$⊢\phi \to FFnA$$
	fmptunsnop.2	$$⊢\phi \to X\in A$$
	fmptunsnop.3	$$⊢\phi \to Y\in B$$
Assertion	fmptunsnop	$$⊢\phi \to \left(x\in A⟼if\left(x=X,Y,F\left(x\right)\right)\right)=\left({F\upharpoonright }_{\left(A\setminus \left\{X\right\}\right)}\right)\cup \left\{⟨X,Y⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fmptunsnop.1	$$⊢\phi \to FFnA$$
2		fmptunsnop.2	$$⊢\phi \to X\in A$$
3		fmptunsnop.3	$$⊢\phi \to Y\in B$$
4		mptun	$$⊢\left(x\in \left(\left(A\setminus \left\{X\right\}\right)\cup \left\{X\right\}\right)⟼if\left(x=X,Y,F\left(x\right)\right)\right)=\left(x\in \left(A\setminus \left\{X\right\}\right)⟼if\left(x=X,Y,F\left(x\right)\right)\right)\cup \left(x\in \left\{X\right\}⟼if\left(x=X,Y,F\left(x\right)\right)\right)$$
5		difsnid	$$⊢X\in A\to \left(A\setminus \left\{X\right\}\right)\cup \left\{X\right\}=A$$
6	2 5	syl	$$⊢\phi \to \left(A\setminus \left\{X\right\}\right)\cup \left\{X\right\}=A$$
7	6	mpteq1d	$$⊢\phi \to \left(x\in \left(\left(A\setminus \left\{X\right\}\right)\cup \left\{X\right\}\right)⟼if\left(x=X,Y,F\left(x\right)\right)\right)=\left(x\in A⟼if\left(x=X,Y,F\left(x\right)\right)\right)$$
8		eldifsni	$$⊢x\in \left(A\setminus \left\{X\right\}\right)\to x\ne X$$
9	8	adantl	$$⊢\left(\phi \wedge x\in \left(A\setminus \left\{X\right\}\right)\right)\to x\ne X$$
10	9	neneqd	$$⊢\left(\phi \wedge x\in \left(A\setminus \left\{X\right\}\right)\right)\to \neg x=X$$
11	10	iffalsed	$$⊢\left(\phi \wedge x\in \left(A\setminus \left\{X\right\}\right)\right)\to if\left(x=X,Y,F\left(x\right)\right)=F\left(x\right)$$
12	11	mpteq2dva	$$⊢\phi \to \left(x\in \left(A\setminus \left\{X\right\}\right)⟼if\left(x=X,Y,F\left(x\right)\right)\right)=\left(x\in \left(A\setminus \left\{X\right\}\right)⟼F\left(x\right)\right)$$
13		dffn3	$$⊢FFnA\leftrightarrow F:A⟶\mathrm{ran}F$$
14	1 13	sylib	$$⊢\phi \to F:A⟶\mathrm{ran}F$$
15		difssd	$$⊢\phi \to A\setminus \left\{X\right\}\subseteq A$$
16	14 15	feqresmpt	$$⊢\phi \to {F\upharpoonright }_{\left(A\setminus \left\{X\right\}\right)}=\left(x\in \left(A\setminus \left\{X\right\}\right)⟼F\left(x\right)\right)$$
17	12 16	eqtr4d	$$⊢\phi \to \left(x\in \left(A\setminus \left\{X\right\}\right)⟼if\left(x=X,Y,F\left(x\right)\right)\right)={F\upharpoonright }_{\left(A\setminus \left\{X\right\}\right)}$$
18		iftrue	$$⊢x=X\to if\left(x=X,Y,F\left(x\right)\right)=Y$$
19	18	adantl	$$⊢\left(\phi \wedge x=X\right)\to if\left(x=X,Y,F\left(x\right)\right)=Y$$
20	19 2 3	fmptsnd	$$⊢\phi \to \left\{⟨X,Y⟩\right\}=\left(x\in \left\{X\right\}⟼if\left(x=X,Y,F\left(x\right)\right)\right)$$
21	20	eqcomd	$$⊢\phi \to \left(x\in \left\{X\right\}⟼if\left(x=X,Y,F\left(x\right)\right)\right)=\left\{⟨X,Y⟩\right\}$$
22	17 21	uneq12d	$$⊢\phi \to \left(x\in \left(A\setminus \left\{X\right\}\right)⟼if\left(x=X,Y,F\left(x\right)\right)\right)\cup \left(x\in \left\{X\right\}⟼if\left(x=X,Y,F\left(x\right)\right)\right)=\left({F\upharpoonright }_{\left(A\setminus \left\{X\right\}\right)}\right)\cup \left\{⟨X,Y⟩\right\}$$
23	4 7 22	3eqtr3a	$$⊢\phi \to \left(x\in A⟼if\left(x=X,Y,F\left(x\right)\right)\right)=\left({F\upharpoonright }_{\left(A\setminus \left\{X\right\}\right)}\right)\cup \left\{⟨X,Y⟩\right\}$$