[proofplan] Work inside the first-order natural-deduction proof system specified in the theorem statement, so the universal-elimination rule is an available inference rule with its usual capture-avoidance side condition. Start with a derivation of $\forall x\,A(x)$ from the open assumptions $\Gamma$. Since $t$ is free for $x$ in $A(x)$, the substitution instance $A(t)$, equivalently $A[t/x]$, is a legitimate instance of universal elimination. Appending one application of that rule to the given derivation produces a derivation of $A(t)$ with exactly the same open assumptions. [/proofplan] [step:Choose a derivation of the universally quantified formula] Assume $\Gamma \vdash \forall x\,A(x)$ in the fixed first-order natural-deduction proof system. By the meaning of derivability, there exists a derivation $\mathcal{D}$ whose conclusion is $\forall x\,A(x)$ and whose open assumptions are all contained in $\Gamma$. [guided] The hypothesis $\Gamma \vdash \forall x\,A(x)$ is a statement about the existence of a formal derivation in the fixed first-order natural-deduction proof system. Thus we fix one such derivation and name it $\mathcal{D}$. Its final line is the formula $\forall x\,A(x)$, and every undischarged assumption occurring in $\mathcal{D}$ belongs to $\Gamma$. This is the object to which we will append one more inference. [/guided] [/step] [step:Apply universal elimination with the capture-free substitution instance] The universal-elimination rule is available in the fixed proof system by the theorem statement. It permits the inference \begin{align*} \frac{\forall x\,A(x)}{A[t/x]} \end{align*} provided that $t$ is free for $x$ in $A(x)$. This side condition is exactly one of the hypotheses. Since $A[t/x]$ denotes the result of replacing the free occurrences of $x$ in $A(x)$ by $t$, we have $A[t/x] = A(t)$ by the notation of the theorem statement. Therefore, applying universal elimination to the last line of $\mathcal{D}$ gives a derivation whose final conclusion is $A(t)$. [guided] The central rule used here is not an additional metatheorem; it is the universal-elimination inference rule included in the fixed first-order natural-deduction proof system named in the theorem statement. That rule permits the inference \begin{align*} \frac{\forall x\,A(x)}{A[t/x]} \end{align*} when $t$ is free for $x$ in $A(x)$. The only syntactic issue in this rule is variable capture. The condition that $t$ is free for $x$ in $A(x)$ means that replacing the free occurrences of $x$ in $A(x)$ by $t$ creates the formula $A[t/x]$ without causing any free variable of $t$ to become bound by a quantifier already present in $A(x)$. Hence $A[t/x]$ is an allowed substitution instance of $A(x)$. By the theorem statement's notation, this substitution instance is $A(t)$. Now apply the universal-elimination inference rule to the final formula of $\mathcal{D}$: \begin{align*} \frac{\forall x\,A(x)}{A[t/x]}. \end{align*} Since the premise $\forall x\,A(x)$ is already the conclusion of $\mathcal{D}$, appending this single inference produces a formal derivation ending in $A[t/x] = A(t)$. [/guided] [/step] [step:Verify that the open assumptions are unchanged] The appended universal-elimination inference introduces no new assumption and discharges no existing assumption. Hence the open assumptions of the extended derivation are exactly the open assumptions of $\mathcal{D}$, and these are contained in $\Gamma$. Since $A[t/x] = A(t)$, we obtain \begin{align*} \Gamma \vdash A(t). \end{align*} This proves the admissibility of [universal instantiation](/theorems/4637). [guided] It remains to check that adding the last inference has not changed the assumptions on which the derivation depends. Universal elimination is a one-premise inference rule: it takes the already-derived formula $\forall x\,A(x)$ as its premise and produces the substitution instance $A[t/x]$ as its conclusion. It introduces no new open assumption and it discharges no existing assumption. Therefore the open assumptions of the extended derivation are exactly the open assumptions of the original derivation $\mathcal{D}$. Those open assumptions are contained in $\Gamma$ by the choice of $\mathcal{D}$. Since the final formula of the extended derivation is $A[t/x] = A(t)$, the definition of derivability gives \begin{align*} \Gamma \vdash A(t). \end{align*} This is precisely the claimed admissibility of universal instantiation. [/guided] [/step]