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

Metamath Proof Explorer

Theorem funresd

Description: A restriction of a function is a function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

		Ref	Expression
	Hypothesis	funresd.1	$⊢ φ \to Fun F$
	Assertion	funresd	$⊢ φ \to Fun ({F ↾}_{A})$

Step	Hyp	Ref	Expression
1		funresd.1	$⊢ φ \to Fun F$
2		funres	$⊢ Fun F \to Fun ({F ↾}_{A})$
3	1 2	syl	$⊢ φ \to Fun ({F ↾}_{A})$