Theorem fnsnsplit

Description: Split a function into a single point and all the rest. (Contributed by Stefan O'Rear, 27-Feb-2015)

	Ref	Expression
Assertion	fnsnsplit	|- ( ( F Fn A /\ X e. A ) -> F = ( ( F |` ( A \ { X } ) ) u. { <. X , ( F ` X ) >. } ) )

Proof

Step	Hyp	Ref	Expression
1		fnresdm	|- ( F Fn A -> ( F |` A ) = F )
2	1	adantr	|- ( ( F Fn A /\ X e. A ) -> ( F |` A ) = F )
3		resundi	|- ( F |` ( ( A \ { X } ) u. { X } ) ) = ( ( F |` ( A \ { X } ) ) u. ( F |` { X } ) )
4		difsnid	|- ( X e. A -> ( ( A \ { X } ) u. { X } ) = A )
5	4	adantl	|- ( ( F Fn A /\ X e. A ) -> ( ( A \ { X } ) u. { X } ) = A )
6	5	reseq2d	|- ( ( F Fn A /\ X e. A ) -> ( F |` ( ( A \ { X } ) u. { X } ) ) = ( F |` A ) )
7		fnressn	|- ( ( F Fn A /\ X e. A ) -> ( F |` { X } ) = { <. X , ( F ` X ) >. } )
8	7	uneq2d	|- ( ( F Fn A /\ X e. A ) -> ( ( F |` ( A \ { X } ) ) u. ( F |` { X } ) ) = ( ( F |` ( A \ { X } ) ) u. { <. X , ( F ` X ) >. } ) )
9	3 6 8	3eqtr3a	|- ( ( F Fn A /\ X e. A ) -> ( F |` A ) = ( ( F |` ( A \ { X } ) ) u. { <. X , ( F ` X ) >. } ) )
10	2 9	eqtr3d	|- ( ( F Fn A /\ X e. A ) -> F = ( ( F |` ( A \ { X } ) ) u. { <. X , ( F ` X ) >. } ) )