Theorem fnssresb

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

	Ref	Expression
Assertion	fnssresb	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ 𝐵 ) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		df-fn	⊢ ( ( 𝐹 ↾ 𝐵 ) Fn 𝐵 ↔ ( Fun ( 𝐹 ↾ 𝐵 ) ∧ dom ( 𝐹 ↾ 𝐵 ) = 𝐵 ) )
2		fnfun	⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
3		funres	⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ 𝐵 ) )
4	2 3	syl	⊢ ( 𝐹 Fn 𝐴 → Fun ( 𝐹 ↾ 𝐵 ) )
5	4	biantrurd	⊢ ( 𝐹 Fn 𝐴 → ( dom ( 𝐹 ↾ 𝐵 ) = 𝐵 ↔ ( Fun ( 𝐹 ↾ 𝐵 ) ∧ dom ( 𝐹 ↾ 𝐵 ) = 𝐵 ) ) )
6		ssdmres	⊢ ( 𝐵 ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ 𝐵 ) = 𝐵 )
7		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
8	7	sseq2d	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ⊆ dom 𝐹 ↔ 𝐵 ⊆ 𝐴 ) )
9	6 8	bitr3id	⊢ ( 𝐹 Fn 𝐴 → ( dom ( 𝐹 ↾ 𝐵 ) = 𝐵 ↔ 𝐵 ⊆ 𝐴 ) )
10	5 9	bitr3d	⊢ ( 𝐹 Fn 𝐴 → ( ( Fun ( 𝐹 ↾ 𝐵 ) ∧ dom ( 𝐹 ↾ 𝐵 ) = 𝐵 ) ↔ 𝐵 ⊆ 𝐴 ) )
11	1 10	syl5bb	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ 𝐵 ) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴 ) )