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	$$⊢\phi \to A\subseteq B$$
	rlimres2.2	$$⊢\phi \to \left(x\in B⟼C\right)\underset{ℝ}{⇝}D$$
Assertion	rlimres2	$$⊢\phi \to \left(x\in A⟼C\right)\underset{ℝ}{⇝}D$$

Proof

Step	Hyp	Ref	Expression
1		rlimres2.1	$$⊢\phi \to A\subseteq B$$
2		rlimres2.2	$$⊢\phi \to \left(x\in B⟼C\right)\underset{ℝ}{⇝}D$$
3	1	resmptd	$$⊢\phi \to {\left(x\in B⟼C\right)\upharpoonright }_A=\left(x\in A⟼C\right)$$
4		rlimres	$$⊢\left(x\in B⟼C\right)\underset{ℝ}{⇝}D\to \left({\left(x\in B⟼C\right)\upharpoonright }_A\right)\underset{ℝ}{⇝}D$$
5	2 4	syl	$$⊢\phi \to \left({\left(x\in B⟼C\right)\upharpoonright }_A\right)\underset{ℝ}{⇝}D$$
6	3 5	eqbrtrrd	$$⊢\phi \to \left(x\in A⟼C\right)\underset{ℝ}{⇝}D$$