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