This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )