Exchangable universal and existential quantification While playing around with the coq prover, I realized that two quantifiers can be exchanged under certain condition:
$$
\forall x. P(x) \to Q \Leftrightarrow (\exists x. P(x)) \to Q
$$
The condition is that $Q$ must not mention $x$ directly(but there can be other connections with $P$ in general).
How should I interpret this logically and verbally? I don't find it's intuitive but this relation is correct.
The counterintuitive part is on right side, I am just talking about a very specific $x$ that satisfy $P$, while it's the same as if I talk about all $x$s as long as my conclusion doesn't mention it.

Coq proof as following:
Goal forall (P : Type -> Prop) (Q : Prop),
  (forall x, P(x) -> Q) <-> ((exists x, P(x)) -> Q).
Proof.
  intros. split.
  - intros. destruct H0. eauto.
  - intros. eauto.
Qed.

 A: Let's suppose first that $Q$ might contain $x$ as a free variable. In this case, the formula $\forall x.\,P(x) \to Q(x)$ says that for any value of $x$, if $P(x)$ is true, then $Q(x)$ is true.
Unwrapping this slightly, this means that for any value of $x$, the formula $P(x) \to Q(x)$ is true. As such, for a fixed value of $x$, if you wanted to prove that $Q(x)$ is true, all you'd have to do is prove that $P(x)$ is true for that particular value of $x$.
Now suppose $Q$ doesn't contain $x$ as a free variable. The above reasoning still holds: for any fixed value of $x$, if you prove that $P(x)$ is true, then it follows that $Q$ is true.
But this is exactly to say that if, for some fixed value of $x$, you prove that $P(x)$ is true—that is, if $\exists x.\, P(x)$ is true—then you can deduce that $Q$ is true. As such, the formula $(\exists x.\, P(x)) \to Q$ is true.
The reasoning why the converse holds is similar.

Generally speaking, the implication operator $A \to B$ is contravariant in $A$ and covariant in $B$.
Covariance in the second argument means that the operators ${\wedge},{\vee}$ and the quantifiers ${\forall},{\exists}$ in the second argument distribute over $\to$; for example $P \to \forall x.\, Q(x)$ is equivalent to $\forall x.\, [P \to Q(x)]$ (provided $x$ is not free in $P$) and $P \to Q \wedge R$ is equivalent to $(P \to Q) \wedge (P \to R)$.
Contravariance in the first argument means the operators ${\wedge},{\vee}$ and the quantifiers ${\forall},{\exists}$ in the first argument distribute over $\to$, except they have to be replaced by their duals; for example $(\forall x.\, P(x)) \to Q$ is equivalent to $\exists x.\, (P(x) \to Q)$ (provided $x$ is not free in $Q$) and $(P \wedge Q) \to R$ is equivalent to $(P \to R) \vee (Q \to R)$. (The question you ask is another instance of this.)
A: Here's a somewhat different perspective that is especially relevant as you are working in Coq.
The equivalence is constructively true. (You're proof is a witness to this fact as Coq's logic is constructive by default.) We can thus apply a constructive reading to it a la BHK/CH. In this reading, a proof of $P \to Q$ is thought of as a function that takes proofs of $P$ and produces proofs of $Q$. Similarly, $\forall x\!:\!X.\!P(x)$ is thought of as a function that takes values of $X$ and produces proofs of $P(x)$. Finally, $\exists x\!:\!X.\!P(x)$ is constructively witnessed meaning we need to actually have a value of $X$ for which $P(x)$ holds, i.e. $\exists x\!:\!X.\!P(x)$ is a pair of a value of $X$ and a proof of $P(x)$.
With this perspective, your equivalence is simply a (dependently typed) variation of the currying isomorphism: $$(A\times B \to C) \cong (A \to (B \to C))$$ Indeed the proof term that your proof script produces is essentially: $$\big\langle\lambda f\!:(\!\forall x.P(x)\to Q).\!\lambda\langle x,p\rangle.\!f(x)(p),\ \lambda g\!:\!((\exists x.P(x))\to Q).\!\lambda x.\!\lambda p.\!g(\langle x,p\rangle)\big\rangle$$
You can read the consequence of this as: For a proof of $Q$ from $x$ and a proof of $P(x)$, we can either take the parameters ($x$ and the proof of $P(x)$) one at a time or paired together.
A: The statement is a generalization of the primitive concept:
$$\bigg( (A \to Q) \land (B \to Q) \bigg) \equiv \bigg((A \lor B) \to Q\bigg)$$
Linguistically, if one person tells you "If hamburgers are on the menu then I'll leave a tip, and if subs are on the menu then I'll leave a tip", and a second person tells you "If hamburgers are on the menu or if subs are on the menu, then I'll leave a tip" then they have both told you the same thing.  So generalizing the example to 
$$\bigg(\forall x ~(Px \to Q)\bigg) \equiv \bigg( (\exists x ~Px) \to Q \bigg)$$
One person tells you "For every kind of sandwich, if it is one the menu then I'll leave a tip".  Second person tells you "If some kind of sandwich is on the menu, then I'll leave a tip".  Both said the same thing.
A: To grok the statements, consider their contrapositions.


*

*$\forall x~(P(x)\to Q) ~\equiv~ \forall x~(\neg Q\to\neg P(x))$ 

*$(\exists x~P(x))\to Q~\equiv~\neg Q\to\neg(\exists x~P(x))$


It should be clear that both expressions state that: if $Q$ is false, then $P(x)$ is never true.
And if $x$ is not contained free within $Q$, we can readily prove the distribution*: $\forall x~(\neg Q\to\neg P(x))~\equiv~\neg Q\to(\forall x~\neg P(x))$
$\tiny\text{(* By universal elimination, assuming not Q, conditional elimination, universal introduction, and conditional introduction to discharge the assumption, and vice versa to demonstrate equivalence.)}$
A: Summarizing others' ideas here, and to provide a slightly different language here, I can also state such fact by interpreting it in algebraic data type, which can be associated with logic by Curry-Howard Isomorphism.
$\forall  x. P(x) \to Q \Leftrightarrow (Q^{P(x)})^\Sigma, for\ x \in \Sigma$
However, that subsequently becomes
$(Q^{P(x)})^\Sigma = Q^{\sum_{x\in \Sigma}P(x)}$
and $\sum_{x\in \Sigma}P(x)$ is exactly dependent sum, which corresponds to existential quantification in formal logic. So
$\Leftrightarrow (\sum_{x\in \Sigma}P(x)) \to Q \Leftrightarrow (\exists x. P(x)) \to Q$
