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	|- ( ph -> A C_ B )
	rlimres2.2	|- ( ph -> ( x e. B |-> C ) ~~>r D )
Assertion	rlimres2	|- ( ph -> ( x e. A |-> C ) ~~>r D )

Proof

Step	Hyp	Ref	Expression
1		rlimres2.1	|- ( ph -> A C_ B )
2		rlimres2.2	|- ( ph -> ( x e. B |-> C ) ~~>r D )
3	1	resmptd	|- ( ph -> ( ( x e. B |-> C ) |` A ) = ( x e. A |-> C ) )
4		rlimres	|- ( ( x e. B |-> C ) ~~>r D -> ( ( x e. B |-> C ) |` A ) ~~>r D )
5	2 4	syl	|- ( ph -> ( ( x e. B |-> C ) |` A ) ~~>r D )
6	3 5	eqbrtrrd	|- ( ph -> ( x e. A |-> C ) ~~>r D )