Theorem fmptap

Description: Append an additional value to a function. (Contributed by NM, 6-Jun-2006) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypotheses	fmptap.0a	|- A e. _V
	fmptap.0b	|- B e. _V
	fmptap.1	|- ( R u. { A } ) = S
	fmptap.2	|- ( x = A -> C = B )
Assertion	fmptap	|- ( ( x e. R |-> C ) u. { <. A , B >. } ) = ( x e. S |-> C )

Proof

Step	Hyp	Ref	Expression
1		fmptap.0a	|- A e. _V
2		fmptap.0b	|- B e. _V
3		fmptap.1	|- ( R u. { A } ) = S
4		fmptap.2	|- ( x = A -> C = B )
5		fmptsn	|- ( ( A e. _V /\ B e. _V ) -> { <. A , B >. } = ( x e. { A } |-> B ) )
6	1 2 5	mp2an	|- { <. A , B >. } = ( x e. { A } |-> B )
7		elsni	|- ( x e. { A } -> x = A )
8	7 4	syl	|- ( x e. { A } -> C = B )
9	8	mpteq2ia	|- ( x e. { A } |-> C ) = ( x e. { A } |-> B )
10	6 9	eqtr4i	|- { <. A , B >. } = ( x e. { A } |-> C )
11	10	uneq2i	|- ( ( x e. R |-> C ) u. { <. A , B >. } ) = ( ( x e. R |-> C ) u. ( x e. { A } |-> C ) )
12		mptun	|- ( x e. ( R u. { A } ) |-> C ) = ( ( x e. R |-> C ) u. ( x e. { A } |-> C ) )
13	3	mpteq1i	|- ( x e. ( R u. { A } ) |-> C ) = ( x e. S |-> C )
14	11 12 13	3eqtr2i	|- ( ( x e. R |-> C ) u. { <. A , B >. } ) = ( x e. S |-> C )