[proofplan] We combine the given derivation of $\exists x\,A(x)$ from $\Gamma$ with the given derivation of $C$ from $\Delta$ and the temporary witness assumption $A(a)$. The [existential elimination rule](/theorems/4640) permits exactly this combination, provided the witness variable $a$ is fresh for the undischarged assumptions and the conclusion. The freshness hypotheses ensure the eigenvariable condition is satisfied, so the temporary assumption $A(a)$ is discharged and the remaining undischarged assumptions are precisely those from $\Gamma$ and $\Delta$. [/proofplan] [step:Choose derivations witnessing the two hypotheses] Let $\mathcal{D}_1$ be a derivation whose undischarged assumptions all belong to $\Gamma$ and whose conclusion is $\exists x\,A(x)$. Let $\mathcal{D}_2$ be a derivation whose undischarged assumptions all belong to $\Delta \cup \{A(a)\}$ and whose conclusion is $C$. The first derivation exists because $\Gamma \vdash \exists x\,A(x)$. The second derivation exists because $\Delta,A(a) \vdash C$. [/step] [step:Verify the eigenvariable condition for existential elimination] The existential elimination rule requires that the temporary witness variable $a$ not occur free in any undischarged assumption that remains after discharging $A(a)$, and not occur free in the conclusion $C$. After the intended discharge, the remaining undischarged assumptions are exactly the assumptions from $\Gamma$ in $\mathcal{D}_1$ and the assumptions from $\Delta$ in $\mathcal{D}_2$. By hypothesis, $a$ does not occur free in any formula of $\Gamma$, in any formula of $\Delta$, or in $C$. Hence the eigenvariable side condition for existential elimination is satisfied. [/step] [step:Apply existential elimination and discharge only the witness assumption] Apply existential elimination to $\mathcal{D}_1$ and $\mathcal{D}_2$: from the derivation of $\exists x\,A(x)$ and the derivation of $C$ from the temporary assumption $A(a)$, infer $C$, discharging the occurrence of the assumption $A(a)$ in $\mathcal{D}_2$. No assumption from $\Gamma$ is discharged in this application, because $\mathcal{D}_1$ supplies the existential premise with assumptions in $\Gamma$. No assumption from $\Delta$ is discharged, because existential elimination discharges only the temporary witness assumption $A(a)$. [/step] [step:Identify the undischarged assumptions of the resulting derivation] The resulting derivation has conclusion $C$. Its undischarged assumptions are precisely the undischarged assumptions of $\mathcal{D}_1$ together with the undischarged assumptions of $\mathcal{D}_2$ other than the discharged temporary assumption $A(a)$. Therefore every undischarged assumption of the resulting derivation belongs to $\Gamma \cup \Delta$. Hence there is a derivation of $C$ from assumptions $\Gamma,\Delta$, which is exactly \begin{align*} \Gamma,\Delta \vdash C. \end{align*} This proves the admissibility of existential reasoning under the stated eigenvariable restriction. [/step]