This question is mainly about building intuition.
A lot of the logic rules on First Order Logic make a lot of intuitive sense, like $\lnot\lnot P\equiv P $. Some less, but with an example, everything becomes clear, like $\lnot P \land \left( P \lor Q \right) \Rightarrow Q$. It might seem convoluted first, but with an example, its truth value becomes intuitively clear: "If I say that I have a dog or a cat, and I don't have a dog, then yeah, of course I have a cat".
In the case of the quantifiers ($\forall $ and $\exists$), most of the properties fall on the former, and (at least for me) are quite self evident, like $\forall x \left[ P(a) \rightarrow Q(x) \right] \equiv P(a) \rightarrow \forall x \left[ Q(x) \right]$, but two in specific are not very intuitive without an example. Given a universe $U \neq \emptyset$:
$$[1]: \forall x \left[P(x) \Rightarrow Q(a) \right] \equiv \exists x \left[ P(x) \right] \Rightarrow Q(a) $$
$$[2]: \exists x \left[P(x) \Rightarrow Q(a) \right] \equiv \forall x \left[ P(x) \right] \Rightarrow Q(a) $$
After an example, formula [1] becomes quite clear: "Saying 'For any person, if they are on Mars then Mars is populated' is the same as 'If there is a person on mars, then mars is populated' ". My problem really comes with [2].
I tried thinking of an example or some logic for it, but the best I could come up with was (in reverse order): "Saying 'If all people are in a hotel, then the hotel is full' is the same as 'there's one person which decides if the hotel is full or not (the last one)' ". I don't think that's right though, because one: That example is a biconditional, not an implication. And second: that example doesn't imply $\exists x \left[P(x) \rightarrow Q(a) \right]$, but actually $\exists ! x \left[P(x) \rightarrow Q(a) \right]$.
So my question is: What is an example that can make that concept more intuitively clear?
Edit: Though previously marked as a duplicate of this question, both the question and answer only talk about one side of the equivalence, being: $\exists x \left[P(x) \Rightarrow Q(a) \right] \Rightarrow (\forall x \left[ Q(x) \right] \Rightarrow P(a)) $, but the answer doesn't touch the $ U \neq \emptyset \land (\forall x \left[ Q(x) \right] \Rightarrow P(a) )\Rightarrow \exists x \left[P(x) \Rightarrow Q(a) \right] $ side of things (corrected with $U \neq \emptyset$ and $\Rightarrow$ as pointed out by tkf), so my doubt still remains.
Best Answer
Quoting the answer from tkf:
After some thought, perhaps the example on my question is not bad. Like the one tkf gave, it might just not cover both sides. But, I think that if we think in terms of a deciding person, they are actually equivalent. After building the following proof:
$$ \newcommand{\fitch}[1]{\begin{array}{rlr}#1\end{array}} \newcommand{\fcol}[1]{\begin{array}{r}#1\end{array}} %FirstColumn \newcommand{\scol}[1]{\begin{array}{l}#1\end{array}} %SecondColumn \newcommand{\tcol}[1]{\begin{array}{l}#1\end{array}} %ThirdColumn \newcommand{\subcol}[1]{\begin{array}{|l}#1\end{array}} %SubProofColumn \newcommand{\startsub}{\\[-0.29em]} %adjusts line spacing slightly \newcommand{\endsub}{\startsub} %adjusts line spacing slightly \newcommand{\fendl}{\\[0.044em]} %adjusts line spacing slightly \fitch{ \fcol{1:\fendl 2:\fendl 3:\fendl 4:\fendl 5:\fendl 6:\fendl 7:\fendl 8:\fendl 9:\fendl 10:\fendl 11:\fendl } & \scol { \forall x [P(x)] \rightarrow Q \startsub\subcol{ \lnot \exists x[P(x) \rightarrow Q] \\ \hline \forall x[ \lnot (P(x) \rightarrow Q)] \\ \forall x[ \lnot (\lnot P(x) \lor Q)] \\ \forall x[P(x) \land \lnot Q)] \\ \forall x[P(x)] \\ \lnot Q \\ \lnot Q \rightarrow \lnot \forall x [P(x)] \\ \lnot \forall x[P(x)] \\ \forall x[P(x)] \\ } \endsub \exists x[P(x) \rightarrow Q] \\ } & \tcol{ \text{Premise} \fendl \text{Supposition} \fendl \text{From}\ 2 \fendl \text{From}\ 3 \fendl \text{De Morgan}\ 4 \fendl {\land}\text{E}\ 5 \fendl {\land}\text{E}\ 5 \fendl \text{From}\ 1 \fendl {\rightarrow}\text{E}\ 7,8 \fendl \text{Copy}\ 6 \fendl \text{Contradiction}\ 9,10 \fendl } } $$
and reading it out loud, I think the example indeed makes sense. as: "If you say the hotel is full if everybody is there, you can't say there's no person that ends up filling it (2). That'd mean that even though everybody is in there, since no person will end up filling it, the hotel is not full (5), which is nonsense". We can call that person that ends up filling the hotel, the deciding person. If they are there, the hotel is filled.
Another way to understanding [2] is by changing $\exists x\in X \left[P(x) \implies Q \right]$ to $\exists x\in X \left[\lnot Q \implies \lnot P(x) \right]$, which would lead to the following example: "If you say that the hotel is full if everybody is in there, then if the hotel is not full, someone is not there". That person that is missing from the hotel, that is the deciding person. So what the rule actually says is that, if everybody is required to fill the hotel, a deciding person exists.
Note that who is missing doesn't matter, only that someone is missing, which explains why the rule results in $\exists x\in X \left[P(x) \implies Q \right]$ instead of $\exists ! x\in X \left[P(x) \implies Q \right]$.
So, the TLDR is: [2] is best viewed as two separate examples, but both of them are perfectly equivalent, since both have a deciding person.
From LHS to RHS: "If one person is so big that they fill up the hotel and the hotel stops taking bookings when they come, then if their whole group is booked in the hotel will certainly stop taking bookings."
and from RHS to LHS: "Saying 'If all people are in a hotel, then the hotel is full' is the same as 'there's at least one person (namely, the last) in which, if they decide to enter then the hotel is full' "