$(\forall x)(Ax \Rightarrow Bx) \Rightarrow [(\forall x)Ax \Rightarrow (\forall x)Bx]$?

Question

$(\forall x)(Ax \Rightarrow Bx)$ is same as $(\forall x)[(Ax \land Bx) \lor (\lnot Ax)]$ if for every $x$, $Ax \land Bx$ is true then we get $(\forall x)(Ax)$ true and $(\forall x)(Bx)$ true.

We get $(\forall x)(Ax) \Rightarrow (\forall x)(Bx)$ is true for this case
if for some $x$, $Ax$ is false, then $(Ax \Rightarrow Bx)$ is true, also we have $(\forall x)(Ax)$ is false.

We get $(\forall x)(Ax) \Rightarrow (\forall x)(Bx)$ is true for this case.
So can we prove $(\forall x)(Ax \Rightarrow Bx) \Rightarrow [(\forall x)Ax \Rightarrow (\forall x)Bx]$?

Answer 1

Given $\forall{x}, Ax \rightarrow Bx$ and $\forall{x}, Ax$, it must directly follow by definition of $\rightarrow$ that $\forall{x}, Bx$. Otherwise, if $\exists x, x_0 s.t. \neg Bx_0$, we would get a contradition given that $Ax_0$ is true but $Ax_0 \rightarrow Bx_0$ is false.

Thus, $\forall{x}, Ax \rightarrow Bx \rightarrow (\forall{x}, Ax \rightarrow \forall{x}, Bx)$.