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

Metamath Proof Explorer

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 ) )