fnssresb

Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 10-Oct-2007)

		Ref	Expression
	Assertion	fnssresb	$⊢ F Fn A \to (({F ↾}_{B}) Fn B \leftrightarrow B \subseteq A)$

Step	Hyp	Ref	Expression
1		df-fn	$⊢ ({F ↾}_{B}) Fn B \leftrightarrow (Fun ({F ↾}_{B}) \land dom ({F ↾}_{B}) = B)$
2		fnfun	$⊢ F Fn A \to Fun F$
3	2	funresd	$⊢ F Fn A \to Fun ({F ↾}_{B})$
4	3	biantrurd	$⊢ F Fn A \to (dom ({F ↾}_{B}) = B \leftrightarrow (Fun ({F ↾}_{B}) \land dom ({F ↾}_{B}) = B))$
5		ssdmres	$⊢ B \subseteq dom F \leftrightarrow dom ({F ↾}_{B}) = B$
6		fndm	$⊢ F Fn A \to dom F = A$
7	6	sseq2d	$⊢ F Fn A \to (B \subseteq dom F \leftrightarrow B \subseteq A)$
8	5 7	bitr3id	$⊢ F Fn A \to (dom ({F ↾}_{B}) = B \leftrightarrow B \subseteq A)$
9	4 8	bitr3d	$⊢ F Fn A \to ((Fun ({F ↾}_{B}) \land dom ({F ↾}_{B}) = B) \leftrightarrow B \subseteq A)$
10	1 9	bitrid	$⊢ F Fn A \to (({F ↾}_{B}) Fn B \leftrightarrow B \subseteq A)$

Metamath Proof Explorer