This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fresin2

Description: Restriction of a function with respect to the intersection with its domain. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion fresin2 ⊢ F : A ⟶ B → F ↾ C ∩ A = F ↾ C

Proof

Step Hyp Ref Expression
1 fdm ⊢ F : A ⟶ B → dom ⁡ F = A
2 1 eqcomd ⊢ F : A ⟶ B → A = dom ⁡ F
3 2 ineq2d ⊢ F : A ⟶ B → C ∩ A = C ∩ dom ⁡ F
4 3 reseq2d ⊢ F : A ⟶ B → F ↾ C ∩ A = F ↾ C ∩ dom ⁡ F
5 frel ⊢ F : A ⟶ B → Rel ⁡ F
6 resindm ⊢ Rel ⁡ F → F ↾ C ∩ dom ⁡ F = F ↾ C
7 5 6 syl ⊢ F : A ⟶ B → F ↾ C ∩ dom ⁡ F = F ↾ C
8 4 7 eqtrd ⊢ F : A ⟶ B → F ↾ C ∩ A = F ↾ C