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	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ ( 𝐶 ∩ 𝐴 ) ) = ( 𝐹 ↾ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		fdm	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 = 𝐴 )
2	1	eqcomd	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐴 = dom 𝐹 )
3	2	ineq2d	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐶 ∩ 𝐴 ) = ( 𝐶 ∩ dom 𝐹 ) )
4	3	reseq2d	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ ( 𝐶 ∩ 𝐴 ) ) = ( 𝐹 ↾ ( 𝐶 ∩ dom 𝐹 ) ) )
5		frel	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → Rel 𝐹 )
6		resindm	⊢ ( Rel 𝐹 → ( 𝐹 ↾ ( 𝐶 ∩ dom 𝐹 ) ) = ( 𝐹 ↾ 𝐶 ) )
7	5 6	syl	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ ( 𝐶 ∩ dom 𝐹 ) ) = ( 𝐹 ↾ 𝐶 ) )
8	4 7	eqtrd	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ ( 𝐶 ∩ 𝐴 ) ) = ( 𝐹 ↾ 𝐶 ) )