Theorem funresdfunsn

Description: Restricting a function to a domain without one element of the domain of the function, and adding a pair of this element and the function value of the element results in the function itself. (Contributed by AV, 2-Dec-2018)

	Ref	Expression
Assertion	funresdfunsn	|- ( ( Fun F /\ X e. dom F ) -> ( ( F |` ( _V \ { X } ) ) u. { <. X , ( F ` X ) >. } ) = F )

Proof

Step	Hyp	Ref	Expression
1		funrel	|- ( Fun F -> Rel F )
2		resdmdfsn	|- ( Rel F -> ( F |` ( _V \ { X } ) ) = ( F |` ( dom F \ { X } ) ) )
3	1 2	syl	|- ( Fun F -> ( F |` ( _V \ { X } ) ) = ( F |` ( dom F \ { X } ) ) )
4	3	adantr	|- ( ( Fun F /\ X e. dom F ) -> ( F |` ( _V \ { X } ) ) = ( F |` ( dom F \ { X } ) ) )
5	4	uneq1d	|- ( ( Fun F /\ X e. dom F ) -> ( ( F |` ( _V \ { X } ) ) u. { <. X , ( F ` X ) >. } ) = ( ( F |` ( dom F \ { X } ) ) u. { <. X , ( F ` X ) >. } ) )
6		funfn	|- ( Fun F <-> F Fn dom F )
7		fnsnsplit	|- ( ( F Fn dom F /\ X e. dom F ) -> F = ( ( F |` ( dom F \ { X } ) ) u. { <. X , ( F ` X ) >. } ) )
8	6 7	sylanb	|- ( ( Fun F /\ X e. dom F ) -> F = ( ( F |` ( dom F \ { X } ) ) u. { <. X , ( F ` X ) >. } ) )
9	5 8	eqtr4d	|- ( ( Fun F /\ X e. dom F ) -> ( ( F |` ( _V \ { X } ) ) u. { <. X , ( F ` X ) >. } ) = F )