Theorem feqresmpt

Description: Express a restricted function as a mapping. (Contributed by Mario Carneiro, 18-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		feqmptd.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		feqresmpt.2	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
3	1 2	fssresd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 )
4	3	feqmptd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) = ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ) )
5		fvres	⊢ ( 𝑥 ∈ 𝐶 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
6	5	mpteq2ia	⊢ ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) )
7	4 6	eqtrdi	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) = ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) )