Well-formed formula a theorem in first-order system K

Question

I'm trying to show that the following well formed formula is a theorem of K:

$(\forall{x_i})\sim(A \to B) \to ((\forall{x_i})A \to (\forall{x_i})\sim B)$

Before going any further, I've rewritten it:

$(\forall{x_i})\sim(A \to B) \to (\forall{x_i})(A \to \sim B)$

which is equivalent to:

$(\forall{x_i})(\sim(A \to B) \to (A \to \sim B))$

which is a tautology and as such the wff is a theorem in K. Is this considered a complete proof that the wff is a theorem of K? I could go ahead and use the deduction theorem and the axioms of K but this seems like a faster way, assuming all the formulas above are in fact logically equivalent.

Thanks

Answer 1

Note that $((\forall{x_i})A \to (\forall{x_i})\sim B)$ is not equivalent to $(\forall{x_i})(A \to \sim B)$ If you have one of the $x_i$ for which $A$ is false, the first statement is true because the antecedent is false. For the second, you must have $A$ true for all the $x_i$ and $B$ false for all the $x_i$