Theorem rlimres2

Description: The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014)

	Ref	Expression
Hypotheses	rlimres2.1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	rlimres2.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ⇝𝑟 𝐷 )
Assertion	rlimres2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		rlimres2.1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
2		rlimres2.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ⇝𝑟 𝐷 )
3	1	resmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
4		rlimres	⊢ ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ⇝𝑟 𝐷 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ↾ 𝐴 ) ⇝𝑟 𝐷 )
5	2 4	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ↾ 𝐴 ) ⇝𝑟 𝐷 )
6	3 5	eqbrtrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐷 )