[proofplan]
The proof is semantic. Given an assignment $s$, the term $t$ denotes an element of the structure; this element will be the witness for the existential quantifier. The only point requiring care is that $A[t/x]$ must really express the formula $A$ evaluated after assigning $x$ the value of $t$, and this is exactly what the capture-free substitution condition guarantees.
[/proofplan]
[step:Use the denotation of the substituted term as the witness]
Let $\mathcal{L}$ be a first-order language, let $\operatorname{Var}$ denote the set of variables of $\mathcal{L}$, let $x\in\operatorname{Var}$, let $A$ be an $\mathcal{L}$-formula, and let $t$ be an $\mathcal{L}$-term that is free for $x$ in $A$ in the sense of [capture-free substitution](/page/Capture-Free%20Substitution). Let $\mathcal{M}$ be an $\mathcal{L}$-[structure](/page/Structure) with universe $M$, and let $s:\operatorname{Var}\to M$ be a variable assignment. Define the element
\begin{align*}
a := \llbracket t \rrbracket_{\mathcal{M},s} \in M,
\end{align*}
where $\llbracket t \rrbracket_{\mathcal{M},s}$ denotes the [term denotation](/page/Term%20Denotation) of $t$ in $\mathcal{M}$ under the assignment $s$.
Assume, in the [satisfaction relation](/page/Satisfaction), that
\begin{align*}
\mathcal{M},s\models A[t/x].
\end{align*}
The [Substitution Lemma for Capture-Free Substitution](/page/Substitution%20Lemma) states that if $t$ is free for $x$ in $A$, then for every $\mathcal{L}$-structure $\mathcal{N}$, every variable assignment $r:\operatorname{Var}\to N$ into the universe $N$ of $\mathcal{N}$, and the element $c:=\llbracket t\rrbracket_{\mathcal{N},r}\in N$, one has
\begin{align*}
\mathcal{N},r\models A[t/x]
\quad\Longleftrightarrow\quad
\mathcal{N},r[x:=c]\models A.
\end{align*}
Its hypotheses are satisfied here because $t$ is free for $x$ in $A$ by assumption. Applying the lemma with $\mathcal{N}=\mathcal{M}$, $r=s$, and $c=a$ gives
\begin{align*}
\mathcal{M},s\models A[t/x]
\quad\Longleftrightarrow\quad
\mathcal{M},s[x:=a]\models A,
\end{align*}
where $s[x:=a]:\operatorname{Var}\to M$ is the assignment defined by
\begin{align*}
s[x:=a](y)=
\begin{cases}
a, & y=x,\\
s(y), & y\ne x.
\end{cases}
\end{align*}
Hence
\begin{align*}
\mathcal{M},s[x:=a]\models A.
\end{align*}
By the [semantics of the existential quantifier](/page/Existential%20Quantifier),
\begin{align*}
\mathcal{M},s\models \exists x\,A
\end{align*}
holds exactly when there exists some $b\in M$ such that
\begin{align*}
\mathcal{M},s[x:=b]\models A.
\end{align*}
Taking $b=a$ gives the required witness. Therefore
\begin{align*}
\mathcal{M},s\models \exists x\,A.
\end{align*}
This proves the semantic soundness of the existential introduction rule.
[guided]
Let $\mathcal{L}$ be a first-order language, let $\operatorname{Var}$ denote the set of variables of $\mathcal{L}$, let $x\in\operatorname{Var}$, let $A$ be an $\mathcal{L}$-formula, and let $t$ be an $\mathcal{L}$-term that is free for $x$ in $A$ in the sense of [capture-free substitution](/page/Capture-Free%20Substitution). Let $\mathcal{M}$ be an $\mathcal{L}$-[structure](/page/Structure) with universe $M$, and let $s:\operatorname{Var}\to M$ be a variable assignment. The premise says, in the [satisfaction relation](/page/Satisfaction), that the substituted formula $A[t/x]$ is true under $s$:
\begin{align*}
\mathcal{M},s\models A[t/x].
\end{align*}
The existential conclusion requires a witness for $x$. The natural witness is the object denoted by the term $t$ under the current assignment. Define
\begin{align*}
a := \llbracket t \rrbracket_{\mathcal{M},s}\in M,
\end{align*}
where $\llbracket t \rrbracket_{\mathcal{M},s}$ is the [term denotation](/page/Term%20Denotation) of $t$ in $\mathcal{M}$ under $s$. Now define the modified assignment $s[x:=a]:\operatorname{Var}\to M$ by
\begin{align*}
s[x:=a](y)=
\begin{cases}
a, & y=x,\\
s(y), & y\ne x.
\end{cases}
\end{align*}
The capture-free substitution hypothesis is used here. The [Substitution Lemma for Capture-Free Substitution](/page/Substitution%20Lemma) states that if $t$ is free for $x$ in $A$, then for every $\mathcal{L}$-structure $\mathcal{N}$, every variable assignment $r:\operatorname{Var}\to N$ into the universe $N$ of $\mathcal{N}$, and the element $c:=\llbracket t\rrbracket_{\mathcal{N},r}\in N$, one has
\begin{align*}
\mathcal{N},r\models A[t/x]
\quad\Longleftrightarrow\quad
\mathcal{N},r[x:=c]\models A.
\end{align*}
We may apply this lemma because $t$ is free for $x$ in $A$ by assumption: replacing free occurrences of $x$ by $t$ does not cause any variable of $t$ to become bound inside $A$. Applying the lemma with $\mathcal{N}=\mathcal{M}$, $r=s$, and $c=a$ gives
\begin{align*}
\mathcal{M},s\models A[t/x]
\quad\Longleftrightarrow\quad
\mathcal{M},s[x:=a]\models A.
\end{align*}
Since the left-hand side holds by hypothesis, we obtain
\begin{align*}
\mathcal{M},s[x:=a]\models A.
\end{align*}
Finally, by the [semantics of the existential quantifier](/page/Existential%20Quantifier),
\begin{align*}
\mathcal{M},s\models \exists x\,A
\end{align*}
means that there exists an element $b\in M$ such that
\begin{align*}
\mathcal{M},s[x:=b]\models A.
\end{align*}
The element $a=\llbracket t \rrbracket_{\mathcal{M},s}$ is such an element. Hence
\begin{align*}
\mathcal{M},s\models \exists x\,A.
\end{align*}
This establishes the soundness of the rule.
[/guided]
[/step]
