Metamath Proof Explorer

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 \land X \in dom F) \to ({F ↾}_{(V ∖ \{X\})}) \cup \{⟨X, F (X)⟩\} = F$

Proof

Step	Hyp	Ref	Expression
1		funrel	$⊢ Fun F \to Rel F$
2		resdmdfsn	$⊢ Rel F \to {F ↾}_{(V ∖ \{X\})} = {F ↾}_{(dom F ∖ \{X\})}$
3	1 2	syl	$⊢ Fun F \to {F ↾}_{(V ∖ \{X\})} = {F ↾}_{(dom F ∖ \{X\})}$
4	3	adantr	$⊢ (Fun F \land X \in dom F) \to {F ↾}_{(V ∖ \{X\})} = {F ↾}_{(dom F ∖ \{X\})}$
5	4	uneq1d	$⊢ (Fun F \land X \in dom F) \to ({F ↾}_{(V ∖ \{X\})}) \cup \{⟨X, F (X)⟩\} = ({F ↾}_{(dom F ∖ \{X\})}) \cup \{⟨X, F (X)⟩\}$
6		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
7		fnsnsplit	$⊢ (F Fn dom F \land X \in dom F) \to F = ({F ↾}_{(dom F ∖ \{X\})}) \cup \{⟨X, F (X)⟩\}$
8	6 7	sylanb	$⊢ (Fun F \land X \in dom F) \to F = ({F ↾}_{(dom F ∖ \{X\})}) \cup \{⟨X, F (X)⟩\}$
9	5 8	eqtr4d	$⊢ (Fun F \land X \in dom F) \to ({F ↾}_{(V ∖ \{X\})}) \cup \{⟨X, F (X)⟩\} = F$