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 2 funresd ⊢ F Fn A → Fun ⁡ F ↾ B
4 3 biantrurd ⊢ F Fn A → dom ⁡ F ↾ B = B ↔ Fun ⁡ F ↾ B ∧ dom ⁡ F ↾ B = B
5 ssdmres ⊢ B ⊆ dom ⁡ F ↔ dom ⁡ F ↾ B = B
6 fndm ⊢ F Fn A → dom ⁡ F = A
7 6 sseq2d ⊢ F Fn A → B ⊆ dom ⁡ F ↔ B ⊆ A
8 5 7 bitr3id ⊢ F Fn A → dom ⁡ F ↾ B = B ↔ B ⊆ A
9 4 8 bitr3d ⊢ F Fn A → Fun ⁡ F ↾ B ∧ dom ⁡ F ↾ B = B ↔ B ⊆ A
10 1 9 syl5bb ⊢ F Fn A → F ↾ B Fn B ↔ B ⊆ A