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	$$⊢\phi \to \left(x\in A⟼X\right):A\underset{cn}{⟶}D$$
	cnmptlimc.b	$$⊢\phi \to B\in A$$
	cnmptlimc.1	$$⊢x=B\to X=Y$$
Assertion	cnmptlimc	$$⊢\phi \to Y\in \left(\left(x\in A⟼X\right){lim}_{ℂ}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnmptlimc.f	$$⊢\phi \to \left(x\in A⟼X\right):A\underset{cn}{⟶}D$$
2		cnmptlimc.b	$$⊢\phi \to B\in A$$
3		cnmptlimc.1	$$⊢x=B\to X=Y$$
4		eqid	$$⊢\left(x\in A⟼X\right)=\left(x\in A⟼X\right)$$
5	3	eleq1d	$$⊢x=B\to \left(X\in D\leftrightarrow Y\in D\right)$$
6		cncff	$$⊢\left(x\in A⟼X\right):A\underset{cn}{⟶}D\to \left(x\in A⟼X\right):A⟶D$$
7	1 6	syl	$$⊢\phi \to \left(x\in A⟼X\right):A⟶D$$
8	4	fmpt	$$⊢\forall x\in AX\in D\leftrightarrow \left(x\in A⟼X\right):A⟶D$$
9	7 8	sylibr	$$⊢\phi \to \forall x\in AX\in D$$
10	5 9 2	rspcdva	$$⊢\phi \to Y\in D$$
11	4 3 2 10	fvmptd3	$$⊢\phi \to \left(x\in A⟼X\right)\left(B\right)=Y$$
12	1 2	cnlimci	$$⊢\phi \to \left(x\in A⟼X\right)\left(B\right)\in \left(\left(x\in A⟼X\right){lim}_{ℂ}B\right)$$
13	11 12	eqeltrrd	$$⊢\phi \to Y\in \left(\left(x\in A⟼X\right){lim}_{ℂ}B\right)$$