Theorem resmptf

Description: Restriction of the mapping operation. (Contributed by Thierry Arnoux, 28-Mar-2017)

	Ref	Expression
Hypotheses	resmptf.a	⊢ Ⅎ 𝑥 𝐴
	resmptf.b	⊢ Ⅎ 𝑥 𝐵
Assertion	resmptf	⊢ ( 𝐵 ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐵 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		resmptf.a	⊢ Ⅎ 𝑥 𝐴
2		resmptf.b	⊢ Ⅎ 𝑥 𝐵
3		resmpt	⊢ ( 𝐵 ⊆ 𝐴 → ( ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ↾ 𝐵 ) = ( 𝑦 ∈ 𝐵 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
4		nfcv	⊢ Ⅎ 𝑦 𝐴
5		nfcv	⊢ Ⅎ 𝑦 𝐶
6		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
7		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
8	1 4 5 6 7	cbvmptf	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
9	8	reseq1i	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐵 ) = ( ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ↾ 𝐵 )
10		nfcv	⊢ Ⅎ 𝑦 𝐵
11	2 10 5 6 7	cbvmptf	⊢ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
12	3 9 11	3eqtr4g	⊢ ( 𝐵 ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐵 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )