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	|- ( ph -> A e. V )
	fmptapd.b	|- ( ph -> B e. W )
	fmptapd.s	|- ( ph -> ( R u. { A } ) = S )
	fmptapd.c	|- ( ( ph /\ x = A ) -> C = B )
Assertion	fmptapd	|- ( ph -> ( ( x e. R |-> C ) u. { <. A , B >. } ) = ( x e. S |-> C ) )

Proof

Step	Hyp	Ref	Expression
1		fmptapd.a	|- ( ph -> A e. V )
2		fmptapd.b	|- ( ph -> B e. W )
3		fmptapd.s	|- ( ph -> ( R u. { A } ) = S )
4		fmptapd.c	|- ( ( ph /\ x = A ) -> C = B )
5	4 1 2	fmptsnd	|- ( ph -> { <. A , B >. } = ( x e. { A } |-> C ) )
6	5	uneq2d	|- ( ph -> ( ( x e. R |-> C ) u. { <. A , B >. } ) = ( ( x e. R |-> C ) u. ( x e. { A } |-> C ) ) )
7		mptun	|- ( x e. ( R u. { A } ) |-> C ) = ( ( x e. R |-> C ) u. ( x e. { A } |-> C ) )
8	7	a1i	|- ( ph -> ( x e. ( R u. { A } ) |-> C ) = ( ( x e. R |-> C ) u. ( x e. { A } |-> C ) ) )
9	3	mpteq1d	|- ( ph -> ( x e. ( R u. { A } ) |-> C ) = ( x e. S |-> C ) )
10	6 8 9	3eqtr2d	|- ( ph -> ( ( x e. R |-> C ) u. { <. A , B >. } ) = ( x e. S |-> C ) )