Theorem fundif

Description: A function with removed elements is still a function. (Contributed by AV, 7-Jun-2021) Shorten proof and remove dependency on ax-sep and ax-pr . (Revised by Eric Schmidt, 24-Oct-2026)

	Ref	Expression
Assertion	fundif	$$⊢\mathrm{Fun}F\to \mathrm{Fun}\left(F\setminus A\right)$$

Proof

Step	Hyp	Ref	Expression
1		difss	$$⊢F\setminus A\subseteq F$$
2		funss	$$⊢F\setminus A\subseteq F\to \left(\mathrm{Fun}F\to \mathrm{Fun}\left(F\setminus A\right)\right)$$
3	1 2	ax-mp	$$⊢\mathrm{Fun}F\to \mathrm{Fun}\left(F\setminus A\right)$$