This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funres

Description: A restriction of a function is a function. Compare Exercise 18 of TakeutiZaring p. 25. (Contributed by NM, 16-Aug-1994)

		Ref	Expression
	Assertion	funres	$⊢ Fun F \to Fun ({F ↾}_{A})$

Step	Hyp	Ref	Expression
1		resss	$⊢ {F ↾}_{A} \subseteq F$
2		funss	$⊢ {F ↾}_{A} \subseteq F \to (Fun F \to Fun ({F ↾}_{A}))$
3	1 2	ax-mp	$⊢ Fun F \to Fun ({F ↾}_{A})$