Is this theorem equivalent to "existential instantiation" rule? In Enderton's, There is a theorem called "existential instantiation", it says: 

Assume that the constant symbol $c$ does not occur in $\alpha ,\beta , \Gamma$ and that:
  $$ \Gamma\cup\{\alpha^x_c\}\vdash\beta$$
  Then
  $$\Gamma\cup\{\exists\alpha\}\vdash\beta$$

I've googled the name of the theorem but found that on Wikipedia here for example, It says something else namely, Given $\exists x\alpha$ we can infer $\alpha^x_c$ for some contant symbol $c$ that has not been used before in the deduction. 
It seems that what wikipedia states is the converse of the EL theorems in Enderton's and I don't see how both forms coincede.
Could anyone clarify for me how they state the same fact? 

If you can infer $A$ from $B$, and you have $\Gamma \cup \{A\} \vdash \beta$, then you can conclude that $\Gamma \cup \{B\} \vdash \beta$. (The left-side of a turnstile is like the left-hand side of an implication: strengthening an assumption preserves validity.) Hence there is no conflict between Enderton's rule that operates on an assumption and the rule you found in the Wikipedia that operates on a conclusion.
