In order to better understand the tricky $\exists L$ rule and its eigenvariable requirement from sequent calculus:
$$\Gamma, A[y/x] \vdash \Delta \over \Gamma, \exists xA \vdash \Delta$$
I decided to try proving the below proposition to build my intuition for this rule.
If $A[y/x]\models\Delta$, provided that $y$ does not appear in $A(x)$ and $\Delta$, then $\exists x A(x)\models\Delta$
My attempt:
Suppose $A[y/x]\models\Delta$. Let $M$ be an arbitrary structure with $M\models\exists x A(x)$. Let $v$ be any variable assignment. Then, $M,v\models\exists x A(x)$. Then, there is some $m\in\text{Domain}(M)$ so that $M,v[m/x]\models A(x)$. Let $M'$ be a copy of $M$ with the difference that $y^{M'}=m$. Since $y$ does not appear in $A(x)$, $M',v[m/x]\models A(x)$ by extensionality. It follows that $M',v\models A[y/x]$. Since $v$ is arbitrary, $M'\models A[y/x]$. Since $A[y/x]\models\Delta$, we have $M'\models\Delta$. Since $y$ does not appear in $\Delta$, $M\models\Delta$ by extensionality again. We showed that $\exists x A(x)\models\Delta$, as required.
Is my proof correct?
I don't think so. Rather than trying to disentangle the given attempt (which is a wise exercise in itself), I shall outline a proof in a stripped down way to be compared to.
I shall not annotate the elementary definitions and theorems one by one and not use the generalisations of them to focus on the mainline. They are fairly intuitive and can be found in textbooks covering introductory chapters on model theory; particularly, I recommend Kees Doets' Basic Model Theory (CSLI Publications, 1996). This not widely known book aims at and neatly achieves a clear and concise presentation of the fundamental concepts; one might find a freely available pdf of it circulating on the Web.
In the sequent (in order to stress what is involved is a transformation of sequences of formulas, the symbol ‘$\Rightarrow$’ may be preferable)
$$\Gamma, A(t/x)\Rightarrow\Delta$$
any model of the antecedent, for that reason of $A(t/x)$, must be a model of at least one sentence in $\Delta$ also; otherwise, it would be contrary to our general conception of logical consequence. Likewise, for the $\exists xA$ and $\Delta$ pair. Thus essentially, what we need to show is
$$A(t/x)\rightarrow\exists xA$$
where $t$ is a term substitutable for $x$ in a formula $A$. The succedent $\Delta$ could also be included in the discussion and used to show the significance of the eigenvalue conditions such as by the following illegitimacy ($t$ is supposed to be a closed term as explained below):
$$\begin{array}{c}A(t)\Rightarrow A(t)\\ \hline \exists xA\Rightarrow A(t)\\ \hline \exists xA\Rightarrow\forall xA\end{array}$$
However, it would hardly provide an extra explanatory perspective for the present context.
It should be remarked that $A(t/x)$ is actually not a formula of the object language; it is a metalinguistic expression to signify that the object language formula $A(t)$ is formed by substituting $t$ for $x$ in $A$. So, $A(t)$ is short for $A(t/x)$ only if we argue in the metalanguage.
Now, without loss of generality, we can suppose that the variable $x$ does not appear in $t$; else, the bound variable $x$ could be renamed to a different variable.
Take notice that we shall carry out our argument at the level of the evaluation of the variables (through an arbitrary function $\sigma$).
So, for some structure $\mathfrak{A}$ and an associated (object) assignment $\sigma$, we have the assumption
$$\mathfrak{A}\vDash A(t/x)[\sigma]$$
where $t$ that occurrs in the place of $x$ already designates an object in the universe of the structure. Here is Gentzen's finesse in giving the name eigenvalue to such a term: It has a dual character; it is both a constant (since its value is fixed by $\sigma$) and the argument's (or, derivation's) own variable (in contrast to being a variable overall). A particularly nice construal of eigenvariable is a temporary assumption held in the relevant part of the argument to be discharged thereafter.
Let $\tau$ be the $x$-variant of $\sigma$ such that $\tau(x) =\sigma(t)$. Then,
$$\mathfrak{A}\vDash A(t/x)[\tau]$$
Since under the conditions of the argument,
$$\vDash(x = t)\rightarrow(A\leftrightarrow A(t/x))$$
We get
$$\mathfrak{A}\vDash A[\tau]$$
By the truth condition
$$\mathfrak{A}\vDash\exists xA[\sigma]\iff\mathfrak{A}\vDash A[\tau]\text{ for some }x\text{-variant }\tau\text{ of }\sigma$$
The desired result
$$\mathfrak{A}\vDash\exists x A[\sigma]$$
follows.