Metamath Proof Explorer

Theorem fssres2

Description: Restriction of a restricted function with a subclass of its domain. (Contributed by NM, 21-Jul-2005)

Ref Expression
Assertion fssres2 ⊢ F ↾ A : A ⟶ B ∧ C ⊆ A → F ↾ C : C ⟶ B

Proof

Step Hyp Ref Expression
1 fssres ⊢ F ↾ A : A ⟶ B ∧ C ⊆ A → F ↾ A ↾ C : C ⟶ B
2 resabs1 ⊢ C ⊆ A → F ↾ A ↾ C = F ↾ C
3 2 feq1d ⊢ C ⊆ A → F ↾ A ↾ C : C ⟶ B ↔ F ↾ C : C ⟶ B
4 3 adantl ⊢ F ↾ A : A ⟶ B ∧ C ⊆ A → F ↾ A ↾ C : C ⟶ B ↔ F ↾ C : C ⟶ B
5 1 4 mpbid ⊢ F ↾ A : A ⟶ B ∧ C ⊆ A → F ↾ C : C ⟶ B