Derivation of ∀x (A(x) → B(x)) → (∀x A(x) → ∀x B(x)) in Hilbert style system

Question

While it's quite easy to give a derivation of

$$\forall x ~ \bigg(A(x) \implies B(x)\bigg) \implies \bigg(\forall x~ A(x) \implies \forall x~ B(x)\bigg)$$

in a system that contains the rule of Universal Instantiation, how do you give one in a Hilbert style system like the one in Derek Goldrei's Predicate and Propositional Calculus: A Model of Argument. His Axiom 4,

$$\forall x (A \implies A[t/x]) \tag{Axiom 4}$$

where $t$ is free for $A$, seems to work as a kind of UI, but I'm not that sure. What I'm trying to say is: Does Axiom 4 warrant the inference:

$$\forall x~ (A(x) \implies B(x))$$ $$\downarrow$$ $$\text{(Apply Axiom 4)}$$ $$\downarrow$$ $$(A(x) \implies B(x))$$

...?

Answer 1

1)$∀x (A(x) \to B(x))$ --- premise [a]

2) $∀x A(x)$ --- premise [b]

3) $A(x) \to B(x)$ --- from 1) by Ax.4 and modus ponens

4) $A(x)$ --- from 2) by Ax.4 and modus ponens

5) $B(x)$ --- from 3) and 4) by mp

6) $∀x B(x)$ --- from 5) by Gen rule : $x$ is not free in [a] nor in [b]

7) $\vdash ∀x (A(x) \to B(x)) \to (∀x A(x) \to ∀x B(x))$ --- from 1), 2) and 6) by Deduction theorem twice.

Answer 2

Since "Hilbert style system" is mentioned. It would be better if not using deduction theorem. I can reduce to just use it one time.

$\forall x(Ax\to Bx)$----------------------------Hyp

$\forall x(Ax\to Bx)\to(At\to Bt)$-----------Axiom 5

$\forall xAx\to At$------------------------------Axiom 5

$\forall y(\forall xAx\to By)\to(\forall xAx\to \forall yBy)$-Axiom 6

$At\to Bt$---------------------------------1,2 MP

$\forall xAx\to Bt$-----------------------------3,5 HS

$\forall y(\forall xAx\to By)$------------------------6 Gen

$\forall xAx\to \forall yBy$--------------------------4,7 HS

$\forall xAx\to \forall xBx$--------------------------Replace y by x

$\forall x(Ax\to Bx)\vdash\forall xAx\to \forall xBx$

$\vdash\forall x(Ax\to Bx)\to\forall xAx\to \forall xBx\quad$ Use deduction theorem one time.