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

Metamath Proof Explorer

Theorem fvunsn

Description: Remove an ordered pair not participating in a function value. (Contributed by NM, 1-Oct-2013) (Revised by Mario Carneiro, 28-May-2014)

Ref Expression
Assertion fvunsn 
|- ( B =/= D -> ( ( A u. { <. B , C >. } ) ` D ) = ( A ` D ) )

Proof

Step Hyp Ref Expression
1 resundir 
 |-  ( ( A u. { <. B , C >. } ) |` { D } ) = ( ( A |` { D } ) u. ( { <. B , C >. } |` { D } ) )
2 nelsn 
 |-  ( B =/= D -> -. B e. { D } )
3 ressnop0 
 |-  ( -. B e. { D } -> ( { <. B , C >. } |` { D } ) = (/) )
4 2 3 syl 
 |-  ( B =/= D -> ( { <. B , C >. } |` { D } ) = (/) )
5 4 uneq2d 
 |-  ( B =/= D -> ( ( A |` { D } ) u. ( { <. B , C >. } |` { D } ) ) = ( ( A |` { D } ) u. (/) ) )
6 un0 
 |-  ( ( A |` { D } ) u. (/) ) = ( A |` { D } )
7 5 6 eqtrdi 
 |-  ( B =/= D -> ( ( A |` { D } ) u. ( { <. B , C >. } |` { D } ) ) = ( A |` { D } ) )
8 1 7 eqtrid 
 |-  ( B =/= D -> ( ( A u. { <. B , C >. } ) |` { D } ) = ( A |` { D } ) )
9 8 fveq1d 
 |-  ( B =/= D -> ( ( ( A u. { <. B , C >. } ) |` { D } ) ` D ) = ( ( A |` { D } ) ` D ) )
10 fvressn 
 |-  ( D e. _V -> ( ( ( A u. { <. B , C >. } ) |` { D } ) ` D ) = ( ( A u. { <. B , C >. } ) ` D ) )
11 fvprc 
 |-  ( -. D e. _V -> ( ( ( A u. { <. B , C >. } ) |` { D } ) ` D ) = (/) )
12 fvprc 
 |-  ( -. D e. _V -> ( ( A u. { <. B , C >. } ) ` D ) = (/) )
13 11 12 eqtr4d 
 |-  ( -. D e. _V -> ( ( ( A u. { <. B , C >. } ) |` { D } ) ` D ) = ( ( A u. { <. B , C >. } ) ` D ) )
14 10 13 pm2.61i 
 |-  ( ( ( A u. { <. B , C >. } ) |` { D } ) ` D ) = ( ( A u. { <. B , C >. } ) ` D )
15 fvressn 
 |-  ( D e. _V -> ( ( A |` { D } ) ` D ) = ( A ` D ) )
16 fvprc 
 |-  ( -. D e. _V -> ( ( A |` { D } ) ` D ) = (/) )
17 fvprc 
 |-  ( -. D e. _V -> ( A ` D ) = (/) )
18 16 17 eqtr4d 
 |-  ( -. D e. _V -> ( ( A |` { D } ) ` D ) = ( A ` D ) )
19 15 18 pm2.61i 
 |-  ( ( A |` { D } ) ` D ) = ( A ` D )
20 9 14 19 3eqtr3g 
 |-  ( B =/= D -> ( ( A u. { <. B , C >. } ) ` D ) = ( A ` D ) )