Contraposition followed by universal conditionals

logic

Solution 1:

Assume $\forall x~(Px\to Qx)$.

Take any $x$. Thus by universal instantiation, $Px\to Qx$ holds. You have already shown this is equivalent to $\neg Qx\to\neg Px$.

Since that holds for any $x$, therefore we can generalise. Thus $\forall x~(\neg Qx\to\neg Px)$ is derived from the assumption. $$\forall x~(Px\to Qx) \implies \forall x~(\neg Qx\to\neg Px)$$

The converse can be proven similarly.

$$\forall x~(Px\to Qx) \impliedby \forall x~(\neg Qx\to\neg Px)$$

... and therefore we have established the equivalence.

$$\forall x~(Px\to Qx) \iff \forall x~(\neg Qx\to\neg Px)$$

Related

The binary relation $R:=\subseteq$ with $\operatorname{Domain}(R)=\operatorname{Codomain}(R)=\mathscr{P}(A)$?
From baby Hartshorne: showing the exterior of a circle is segment connected
What does Tate mean when he wrote "Higher dimensional class field theory" in the new preface to the Artin-Tate book and another question?
Completely metrizable implies $G_\delta$
Consequences of the Langlands program
Is the solution to this holiday puzzle unique?
Convergence in $L^p$ of $f_n$ implies convergence in $L^1$ of $|f_n|^p$ and $f_n^p$
are non-degenerate critical points always isolated?
Why do mathematicians care so much about zeta functions?
Curl of a vector in spherical coordinates
Finding shortest distance between a point and a surface
Geometric meaning of a nondegenerate critical point