How to derive $\exists$ Elimination rule in Enderton's system I'm trying to derive the following rule : 

from $α→β$, infer $(∃x)α→β$, provided that $x$ is not free in $β$

in the system of Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001).
The axioms are [see page 112] :

The logical axioms are all generalizations of wffs of the following forms, where $x$ and $у$ are variables and $\alpha$ and $\beta$ are wffs: 
  
  
*
  
*Tautologies; 
  
*$\forall x \alpha \rightarrow \alpha[x/t]$, where $t$ is substitutable for $x$ in $\alpha$;
  
*$\forall x(\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta)$; 
  
*$\alpha \rightarrow \forall x \alpha$, where $x$ does not occur free in $\alpha$.

If the language includes equality, the usual axiom for it are added. 
Modus ponens is the sole rule of inference.

What we can prove in Enderton's system is the following meta-theorem :

if $\Gamma \vdash \alpha \rightarrow \beta$, and $x$ is not free in $\beta$ nor in any formula in $\Gamma$, then : $\Gamma \vdash \exists x \alpha \rightarrow \beta$.

Proof :
We have to start from :
(1) $\Gamma \vdash \alpha \rightarrow \beta$
(2) $\Gamma \vdash \lnot \beta \rightarrow \lnot \alpha$ --- from (1) and Taut, by mp
(3) $\lnot \beta$ --- assumed
(4) $\Gamma, \lnot \beta \vdash \lnot \alpha$.
Now, due to the proviso, we can apply the Gen Th to have :
(5) $\Gamma, \lnot \beta \vdash \forall x \lnot \alpha$
(6) $\Gamma \vdash \lnot \beta \rightarrow \forall x \lnot \alpha$ --- from (3) and (5), by Deduction Theorem
(7) $\Gamma \vdash \lnot \forall x \lnot \alpha \rightarrow \beta$ --- from (6) and Taut, by mp

(8) $\Gamma \vdash \exists x \alpha \rightarrow \beta$ --- abbreviation.

From this theorem, under the same proviso, with $\Gamma = \emptyset$ we have :

(A)   if $\vdash \alpha \rightarrow \beta$, then $\vdash \exists x \alpha \rightarrow \beta$.


Note : these rules are not stated in Enderton's book, but we can easily derive the last one from the theorem in Example (Q3B) [page 122] :

$\vdash (\exists x \alpha \rightarrow \beta) \leftrightarrow \forall x(\alpha \rightarrow \beta)$, provided that $x$ does not occur free in $\beta$.

Proof :
(1) $\vdash \alpha \rightarrow \beta$ 
(2) $\vdash \forall x(\alpha \rightarrow \beta)$ --- by Generalization Theorem [page 117] : if $\Gamma \vdash \varphi$ and $x$ does not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \varphi$, with $\Gamma = \emptyset$. 
(3) $\vdash \exists x \alpha \rightarrow \beta$ --- by (Q3B).
In the same way, from the theorem of Example (Q2A) [page 121] :

$\vdash (\alpha \rightarrow \forall x \beta) \leftrightarrow \forall x(\alpha \rightarrow \beta)$, provided that $x$ does not occur free in $\alpha$,

we can prove the meta-theorem :

(B)   if $\vdash \alpha \rightarrow \beta$, then $\vdash \alpha \rightarrow \forall x \beta$,

with the same proviso.
Of course, we can deduce it from the "more general" meta-theorem :

if $\Gamma \vdash \alpha \rightarrow \beta$, and $x$ is not free in $\alpha$ nor in any formula in $\Gamma$, then : $\Gamma \vdash \alpha \rightarrow \forall x \beta$

which can easily be proved as the other one.
The rules (A) and (B) are the Rules for the Universal and Existential Quantifiers used by David Hilbert & Wilhelm Ackermann, Principles of Mathematical Logic (2nd ed - 1937; see english translation, page 70) and due to Paul Bernays (see footnote); they are used also by S.C.Kleene in his textbooks.
 A: The rule 

from $α→β$, infer $(∃x)α→β$, provided that $x$ is not free in $β$,

without "constraint" on the assumption $\alpha \rightarrow \beta$, is not sound.
Let $\alpha := x = y$ and let $\beta := \forall x (x = y)$; the proviso that $x \notin FV(\beta)$ is satisfied.
If we apply the above rule, we get :

$\exists x (x = y) \rightarrow \forall x (x = y)$.

But this is not true in a domain with more than one element.
Thus, we need the assumption in the form : $\Gamma \vdash \alpha \rightarrow \beta$, whit proviso that $x$ is not free in $β$ nor in any formula in $\Gamma$.
If we try to use in the "unconstrained" form, we are using it with $\Gamma = \{ α→β \}$, and in this case it is nor more true that $x$ is not free in any formula in $\Gamma$.
A: I don't know if this works, and it's definitely not formal since I'm not listing the tautologies properly, but maybe it'll get you thinking.
assumption   (1) (α→β) 

hypothesis   (2) (∃x)α 

axiom 4      (3) [(α→β)→∀x(α→β)]

MP (1), (3)  (4) ∀x(α→β)

axiom 3      (5) [∀x(α→β)→(∀xα→∀xβ)]

MP (5), (4)  (6) (∀xα→∀xβ)

MP, Taut, (6) (7) (¬∀xβ→¬∀xα)  (the tautology is CCpqCNqNp in Polish notation)

MP, Taut, (7) (8) (¬¬∀xβ $\lor$ ¬∀xα) (the tautology is CCpqANpq)

MP, Taut, (8) (9)  (¬¬∀xβ $\lor$ ¬∀x¬¬α) (the tautology is CANNpqANNpNNq)

Def. of ∃     (10) (¬¬∀xβ $\lor$ ∃x¬α)

MP twice, Taut, 10, 2  (11) ¬¬∀xβ (the tautology is CANNpNqCqNNp)

MP Taut, 11 (12) ∀xβ (the tautology is CNNpp)

axiom 2     (13) ∀xα→α[x/t]

MP, 13, 12  (14) β

DT 2-14      (15) ((∃x)α→β)

