Existential Instantiation We know from calculus:if f is a continuous function, for any $x_0$, for any $\epsilon$, there exists a $\delta$ depending on the $\epsilon$ such that if $|x-x_0|< \delta$, then $|f(x)-f(x_0)|< \epsilon$.
Fix $f(x)= x$. We can pick $\delta= \epsilon$ as substitution. Existential instantiation from logic states that $\delta$ must not appear anywhere already in the Knowledge Base. Is there any contradiction?
 A: I think you are asking whether or not you can use existential instantiation to infer from that $\forall \epsilon \exists \delta ...$ statement that $\delta $ can be assumed to be $\epsilon$ in the case $f(x)=x$
I would say no. While in that case it would indeed be true that $|f(x)-f(x_0)|< \epsilon$ if $|x -x_0|<\delta$ and $\delta = \epsilon$, you cannot regard that as a proper instance of existential elimination (once you fix $\epsilon$) for exactly the reason you indicate: we cannot assume that the $\delta $ is some specific object we are already referring to (in this case $\epsilon$). If it turns out that the claim is true with $\delta$ being one of those already defined objects, then you may be able to prove that later on, but you can't assume that just using existential instantiation.
A: In existential instantiation you can instantiate the quantified variable with any available term you like including delta in your example. With universal introduction and existential elimination the situation is different. There you must choose a fresh name. 
To show forall x.phi we choose a fixed but arbitrary c and prove phi[x:=c]. Often one uses x itself for the fresh name. 
To use an assumption exists x.phi we  choose a fixed but arbitrary c and use phi[x:=c]. Often one uses x itself for the fresh name. 
To prove exists x.phi we exhibit any witnessing expression t and prove phi[x:=t]. 
To use an assumption forall x.phi we exhibit any witnessing expression t and use phi[x:=t]. 
To prove forall x0. forall eps.exists delta.forall x.|x-x0| < delta -> |x-x0|< eps
we choose fixed but arbitrary x0 and eps which happen to be fresh at that point. Then pick the witnessing term eps for delta. But note that we could pick any other term, e.g. 1/2*eps. Let's do that for clarity. OK and then we choose y as a fresh name for x (Just for variation). So, we are left with the quantifier-free stmt 
|y-x0|<1/2*eps -> |y-x0|

which is true. 
