Need alternative proof to $ \exists x (k(x) \rightarrow t)$ entails $\forall x (k(x)) \rightarrow t $

Question

I tried to prove $ \exists x (k(x) \rightarrow t)$ entails $\forall x (k(x)) \rightarrow t $ as;

1. $ \exists x (k(x) \rightarrow t)$

2. $ \exists x (\neg k(x) \lor t)$

3. $ \exists x (\neg k(x)) \lor \exists x(t)$

4. $ \neg \forall x (k(x)) \lor \exists x(t)$

5. $ \neg \forall x (k(x)) \lor t$

6. $ \forall x (k(x)) \rightarrow t$

Also tried elimination and introduction on $ \forall$ and $ \exists$ operators, but couldn't find a smarter way out. I guess there should be a much more simpler way, any ideas?

Answer 1

We assume that : $x$ is not free in $t$.

Thus :

$∃x(k(x)→t)$ --- premise

1) $k(x)→t$ --- assumed [a] for $\exists$E

2) $∀xk(x)$ --- assumed [b]

3) $k(x)$ --- from 2) by $\forall$E

4) $t$ --- from 1) and 3) by $\rightarrow$E

5) $∀xk(x) \rightarrow t$ --- from 2) and 4) by $\rightarrow$I, discharging assumption [b]

We have derived $∀xk(x) \rightarrow t$ from assumption [a] : $k(x)→t$. Due to the fact that $x$ is not free in $t$, we have that $x$ is not free in $∀xk(x) \rightarrow t$; thus the proviso for $\exists$E is fulfilled and we can derive :

6) $∀xk(x) \rightarrow t$ --- from 1) and 5) by $\exists$E, discharging assumption [a].

Thus, we have proved :

$∃x(k(x)→t) \vdash ∀xk(x) \rightarrow t$.