Metamath Proof Explorer

Theorem 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 → F ↾ B Fn B ↔ B ⊆ A

Proof

Step Hyp Ref Expression
1 df-fn ⊢ F ↾ B Fn B ↔ Fun ⁡ F ↾ B ∧ dom ⁡ F ↾ B = B
2 fnfun ⊢ F Fn A → Fun ⁡ F
3 funres ⊢ Fun ⁡ F → Fun ⁡ F ↾ B
4 2 3 syl ⊢ F Fn A → Fun ⁡ F ↾ B
5 4 biantrurd ⊢ F Fn A → dom ⁡ F ↾ B = B ↔ Fun ⁡ F ↾ B ∧ dom ⁡ F ↾ B = B
6 ssdmres ⊢ B ⊆ dom ⁡ F ↔ dom ⁡ F ↾ B = B
7 fndm ⊢ F Fn A → dom ⁡ F = A
8 7 sseq2d ⊢ F Fn A → B ⊆ dom ⁡ F ↔ B ⊆ A
9 6 8 syl5bbr ⊢ F Fn A → dom ⁡ F ↾ B = B ↔ B ⊆ A
10 5 9 bitr3d ⊢ F Fn A → Fun ⁡ F ↾ B ∧ dom ⁡ F ↾ B = B ↔ B ⊆ A
11 1 10 syl5bb ⊢ F Fn A → F ↾ B Fn B ↔ B ⊆ A