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	2	funresd	⊢ ( 𝐹 Fn 𝐴 → Fun ( 𝐹 ↾ 𝐵 ) )
4	3	biantrurd	⊢ ( 𝐹 Fn 𝐴 → ( dom ( 𝐹 ↾ 𝐵 ) = 𝐵 ↔ ( Fun ( 𝐹 ↾ 𝐵 ) ∧ dom ( 𝐹 ↾ 𝐵 ) = 𝐵 ) ) )
5		ssdmres	⊢ ( 𝐵 ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ 𝐵 ) = 𝐵 )
6		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
7	6	sseq2d	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ⊆ dom 𝐹 ↔ 𝐵 ⊆ 𝐴 ) )
8	5 7	bitr3id	⊢ ( 𝐹 Fn 𝐴 → ( dom ( 𝐹 ↾ 𝐵 ) = 𝐵 ↔ 𝐵 ⊆ 𝐴 ) )
9	4 8	bitr3d	⊢ ( 𝐹 Fn 𝐴 → ( ( Fun ( 𝐹 ↾ 𝐵 ) ∧ dom ( 𝐹 ↾ 𝐵 ) = 𝐵 ) ↔ 𝐵 ⊆ 𝐴 ) )
10	1 9	bitrid	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ 𝐵 ) Fn 𝐵 ↔ 𝐵 ⊆ 𝐴 ) )