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		resindm	⊢ ( 𝐹 ↾ ( 𝐶 ∩ dom 𝐹 ) ) = ( 𝐹 ↾ 𝐶 )
6	4 5	eqtrdi	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ↾ ( 𝐶 ∩ 𝐴 ) ) = ( 𝐹 ↾ 𝐶 ) )