Theorem fmptapd

Description: Append an additional value to a function. (Contributed by Thierry Arnoux, 3-Jan-2017) (Revised by AV, 10-Aug-2024)

	Ref	Expression
Hypotheses	fmptapd.a	$$⊢\phi \to A\in V$$
	fmptapd.b	$$⊢\phi \to B\in W$$
	fmptapd.s	$$⊢\phi \to R\cup \left\{A\right\}=S$$
	fmptapd.c	$$⊢\left(\phi \wedge x=A\right)\to C=B$$
Assertion	fmptapd	$$⊢\phi \to \left(x\in R⟼C\right)\cup \left\{⟨A,B⟩\right\}=\left(x\in S⟼C\right)$$

Proof

Step	Hyp	Ref	Expression
1		fmptapd.a	$$⊢\phi \to A\in V$$
2		fmptapd.b	$$⊢\phi \to B\in W$$
3		fmptapd.s	$$⊢\phi \to R\cup \left\{A\right\}=S$$
4		fmptapd.c	$$⊢\left(\phi \wedge x=A\right)\to C=B$$
5	4 1 2	fmptsnd	$$⊢\phi \to \left\{⟨A,B⟩\right\}=\left(x\in \left\{A\right\}⟼C\right)$$
6	5	uneq2d	$$⊢\phi \to \left(x\in R⟼C\right)\cup \left\{⟨A,B⟩\right\}=\left(x\in R⟼C\right)\cup \left(x\in \left\{A\right\}⟼C\right)$$
7		mptun	$$⊢\left(x\in \left(R\cup \left\{A\right\}\right)⟼C\right)=\left(x\in R⟼C\right)\cup \left(x\in \left\{A\right\}⟼C\right)$$
8	7	a1i	$$⊢\phi \to \left(x\in \left(R\cup \left\{A\right\}\right)⟼C\right)=\left(x\in R⟼C\right)\cup \left(x\in \left\{A\right\}⟼C\right)$$
9	3	mpteq1d	$$⊢\phi \to \left(x\in \left(R\cup \left\{A\right\}\right)⟼C\right)=\left(x\in S⟼C\right)$$
10	6 8 9	3eqtr2d	$$⊢\phi \to \left(x\in R⟼C\right)\cup \left\{⟨A,B⟩\right\}=\left(x\in S⟼C\right)$$