[proofplan] The entry records the primitive existential-elimination rule schema of natural deduction, so the proof must verify that the displayed hypotheses form a legitimate instance of that schema rather than derive the rule from itself. Starting from a derivation of $\exists x\,A(x)$ and a subderivation of $C$ from the temporary assumption $A(a)$, we check that the undischarged assumptions and the conclusion satisfy the eigenvariable side condition. Once those syntactic conditions are verified, the primitive rule schema yields a derivation of $C$ depending only on $\Gamma \cup \Delta$. [/proofplan] [step:Combine the existential derivation with the temporary witness derivation] By hypothesis, there is a derivation $\pi_1$ whose undischarged assumptions are contained in $\Gamma$ and whose conclusion is $\exists x\,A(x)$: \begin{align*} \pi_1 &: \Gamma \vdash \exists x\,A(x). \end{align*} There is also a derivation $\pi_2$ whose undischarged assumptions are contained in $\Delta \cup \{A(a)\}$ and whose conclusion is $C$: \begin{align*} \pi_2 &: \Delta, A(a) \vdash C. \end{align*} Here $A(a)$ denotes the result of substituting the variable $a$ for the free variable $x$ in $A(x)$, with the usual proviso that the substitution is free for $x$. [/step] [step:Verify the eigenvariable condition for the temporary name $a$] The primitive existential-elimination schema requires that the temporary witness variable $a$ not occur free in the final conclusion and not occur free in any undischarged assumption that remains after the temporary assumption is discharged. The undischarged assumptions of $\pi_1$ are contained in $\Gamma$, and the undischarged assumptions of $\pi_2$ other than $A(a)$ are contained in $\Delta$. By hypothesis, $a$ is not free in $C$ and is not free in any formula belonging to $\Gamma \cup \Delta$. Therefore, after the assumption $A(a)$ is discharged, no remaining open assumption contains $a$ free. This is the exact eigenvariable condition needed for the primitive existential-elimination schema: the derivation of $C$ from $A(a)$ is uniform in the witness name $a$, and the conclusion $C$ does not retain any dependence on that name. [guided] We must check the side condition before applying existential elimination. The temporary assumption $A(a)$ is allowed to contain $a$ free, because $a$ is serving as the temporary witness. However, once that assumption is discharged, the variable $a$ must disappear from every formula that remains active. The remaining assumptions after discharge are the undischarged assumptions inherited from the derivation of $\exists x\,A(x)$, which are contained in $\Gamma$, together with the undischarged assumptions inherited from the subderivation other than $A(a)$, which are contained in $\Delta$. The theorem assumes the stronger condition that $a$ is not free in any formula of $\Gamma \cup \Delta$, and it also assumes that $a$ is not free in $C$. Hence the temporary witness name cannot influence either the final conclusion or any undischarged assumption. This verifies the eigenvariable condition for this instance of the primitive rule schema. [/guided] [/step] [step:Instantiate the primitive existential-elimination schema] We now match the data to the primitive existential-elimination inference schema of the ambient natural-deduction calculus. That schema has a major premise deriving $\exists x\,A(x)$, a minor derivation deriving $C$ from the temporary assumption $A(a)$, and the eigenvariable condition that $a$ is absent from $C$ and from every undischarged assumption not discharged with $A(a)$. The derivation $\pi_1$ supplies the major premise, the derivation $\pi_2$ supplies the minor derivation, and the preceding step verifies the eigenvariable condition. Therefore this is a legitimate instance of the primitive rule schema. The resulting derivation has conclusion $C$ and has undischarged assumptions only among those inherited from $\pi_1$ and from $\pi_2$ other than $A(a)$, hence only among $\Gamma \cup \Delta$. Therefore, \begin{align*} \Gamma \cup \Delta \vdash C. \end{align*} This is the desired conclusion. [guided] We are not deriving existential elimination from existential elimination. The background natural-deduction calculus includes existential elimination as a primitive inference schema, and the task here is to verify that the hypotheses in the theorem form an instance of that schema. The schema requires three pieces of data. First, it requires a major premise deriving an existential statement. The derivation $\pi_1$ provides this because \begin{align*} \pi_1 &: \Gamma \vdash \exists x\,A(x). \end{align*} Second, it requires a minor derivation in which a fresh temporary witness assumption is used to derive the target conclusion. The derivation $\pi_2$ provides this because \begin{align*} \pi_2 &: \Delta, A(a) \vdash C. \end{align*} Third, it requires the eigenvariable side condition: the temporary name $a$ must not occur free in $C$ and must not occur free in any undischarged assumption remaining after $A(a)$ is discharged. The preceding step verified exactly this condition, using the hypotheses that $a$ is not free in $C$ and not free in any formula of $\Gamma \cup \Delta$. Thus the displayed derivations are a legitimate instance of the primitive existential-elimination schema. Applying that primitive schema discharges the temporary assumption $A(a)$ in the minor derivation. The resulting derivation has conclusion $C$, and its undischarged assumptions are only those inherited from $\pi_1$ and from $\pi_2$ other than $A(a)$. These assumptions are contained in $\Gamma \cup \Delta$, so \begin{align*} \Gamma \cup \Delta \vdash C. \end{align*} [/guided] [/step]