Theorem funin

Description: The intersection with a function is a function. Exercise 14(a) of Enderton p. 53. (Contributed by NM, 19-Mar-2004) (Proof shortened by Andrew Salmon, 17-Sep-2011)

	Ref	Expression
Assertion	funin	$$⊢\mathrm{Fun}F\to \mathrm{Fun}\left(F\cap G\right)$$

Proof

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