Theorem feqresmptf

Description: Express a restricted function as a mapping. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	feqresmptf.1	⊢ Ⅎ 𝑥 𝐹
	feqresmptf.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	feqresmptf.3	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
Assertion	feqresmptf	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) = ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		feqresmptf.1	⊢ Ⅎ 𝑥 𝐹
2		feqresmptf.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
3		feqresmptf.3	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
4		nfcv	⊢ Ⅎ 𝑥 𝐶
5	1 4	nfres	⊢ Ⅎ 𝑥 ( 𝐹 ↾ 𝐶 )
6	2 3	fssresd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 )
7	4 5 6	feqmptdf	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) = ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ) )
8		fvres	⊢ ( 𝑥 ∈ 𝐶 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
9	8	mpteq2ia	⊢ ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) )
10	7 9	eqtrdi	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) = ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) )