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

Metamath Proof Explorer

Theorem fnresin1

Description: Restriction of a function's domain with an intersection. (Contributed by NM, 9-Aug-1994)

		Ref	Expression
	Assertion	fnresin1	$⊢ F Fn A \to ({F ↾}_{(A \cap B)}) Fn (A \cap B)$

Step	Hyp	Ref	Expression
1		inss1	$⊢ A \cap B \subseteq A$
2		fnssres	$⊢ (F Fn A \land A \cap B \subseteq A) \to ({F ↾}_{(A \cap B)}) Fn (A \cap B)$
3	1 2	mpan2	$⊢ F Fn A \to ({F ↾}_{(A \cap B)}) Fn (A \cap B)$