Theorem cnmptlimc

Description: If F is a continuous function, then the limit of the function at any point equals its value. (Contributed by Mario Carneiro, 28-Dec-2016)

	Ref	Expression
Hypotheses	cnmptlimc.f	|- ( ph -> ( x e. A |-> X ) e. ( A -cn-> D ) )
	cnmptlimc.b	|- ( ph -> B e. A )
	cnmptlimc.1	|- ( x = B -> X = Y )
Assertion	cnmptlimc	|- ( ph -> Y e. ( ( x e. A |-> X ) limCC B ) )

Proof

Step	Hyp	Ref	Expression
1		cnmptlimc.f	|- ( ph -> ( x e. A |-> X ) e. ( A -cn-> D ) )
2		cnmptlimc.b	|- ( ph -> B e. A )
3		cnmptlimc.1	|- ( x = B -> X = Y )
4		eqid	|- ( x e. A |-> X ) = ( x e. A |-> X )
5	3	eleq1d	|- ( x = B -> ( X e. D <-> Y e. D ) )
6		cncff	|- ( ( x e. A |-> X ) e. ( A -cn-> D ) -> ( x e. A |-> X ) : A --> D )
7	1 6	syl	|- ( ph -> ( x e. A |-> X ) : A --> D )
8	4	fmpt	|- ( A. x e. A X e. D <-> ( x e. A |-> X ) : A --> D )
9	7 8	sylibr	|- ( ph -> A. x e. A X e. D )
10	5 9 2	rspcdva	|- ( ph -> Y e. D )
11	4 3 2 10	fvmptd3	|- ( ph -> ( ( x e. A |-> X ) ` B ) = Y )
12	1 2	cnlimci	|- ( ph -> ( ( x e. A |-> X ) ` B ) e. ( ( x e. A |-> X ) limCC B ) )
13	11 12	eqeltrrd	|- ( ph -> Y e. ( ( x e. A |-> X ) limCC B ) )