Is it possible to convert $\forall$ quantifiers to $\exists$ quantifiers without negation?

I found a statement that says

$$\forall x[P(x) \rightarrow Q] \equiv \exists x[P(x)] \rightarrow Q$$

Where $Q$ is a formula that does not contain $x$.

Correct. This is a true equivalence.

Is there a way to prove the right hand side statement from the left hand side?

Yes. And the other way around as well. See the other Answer. All equivalences in first-order logic can be proven, both mathematically, as well as using a first-order logic formal proof, if that's what you are asking.

I need to know when exactly would the equivalence hold.

Hmm, that's a bit of a weird question. The equivalence holds ... and as with mathematical results, it will therefore always hold.

OK, but given your:

Can we just convert $\forall$ quantifiers to $\exists$.

I assume you real question is:

Are there other cases that are like this where we can change universal and existential quantifiers?

Now, the first thing to note is that we are not just swapping quantifiers. Indeed, it does not hold that:

$$\forall x[P(x) \rightarrow Q] \equiv \exists x[P(x) \rightarrow Q] \text{ WRONG!}$$

nor does it hold that:

$$\forall x[P(x)] \rightarrow Q \equiv \exists x[P(x)] \rightarrow Q \text{ WRONG!}$$

Rather, it is the fact that we changed the scope of the quantifiers (that is, note how the square brackets get moved!) that makes the equivalence hold:

$$\forall x[P(x) \rightarrow Q] \equiv \exists x[P(x)] \rightarrow Q \text{ Correct}$$

Indeed, simply converting existentials to universals will almost never hold true, since in general we do not have that $\forall x \ P(x) \equiv \exists x \ P(x)$\forall.

The only time where you can just swap existentials is where they don't do any work, i.e. where they are null quntifiers. An example of this is that:

$$\forall x \ Q \equiv \exists x \ Q$$

where again $Q$ is a formula that does not contain $x$ (and even this equivalence only hold in logics that make the Assumption of Existential Import: that there is at least element in the domain)

OK, so at this point your question really seems to become: are there other equivalences like:

$$\forall x[P(x) \rightarrow Q] \equiv \exists x[P(x)] \rightarrow Q$$

where you swap quantifiers and change their scope? What are the conditions under which we can make, or cannot make, such a swap?

Well, the relevant set of equivalences that I think you are really looking for are what are called the Prenex Laws. Here they are:

Prenex Laws

Where $x$ is not a free variable in $Q$:

$$ \forall x \ [P(x)] \land Q \Leftrightarrow \forall x [P(x) \land Q]$$

$$ \exists x \ [P(x)] \land Q \Leftrightarrow \exists x [P(x) \land Q]$$

$$ \forall x \ [P(x)] \lor Q \Leftrightarrow \forall x [P(x) \lor Q]$$

$$\exists x \ [P(x)] \lor Q \Leftrightarrow \exists x [P(x) \lor Q]$$

$$\forall x \ [Q] \rightarrow P(x) \Leftrightarrow \forall x [Q\rightarrow P(x)]$$

$$\exists x \ [Q] \rightarrow P(x) \Leftrightarrow \exists x [Q\rightarrow P(x)]$$

$$\exists x \ [P(x)] \rightarrow Q \Leftrightarrow \forall x [P(x) \rightarrow Q]$$

$$\forall x \ [P(x)] \rightarrow Q \Leftrightarrow \exists x [P(x) \rightarrow Q]$$

We recognize your equivalence as the seventh one down, though with the LHS and RHS swapped. It is a little more practical to represent the Laws like this, though, since in practice we often use the Prenex Laws to 'pull out' quantifiers and 'move them over' other logical operators.

The Prenex Laws show that it is ok to change the scope of the quantifiers to include the formula $Q$ (where again, the important criterion is that $Q$ does not contain any free variables $x$!), but that the quantifier swaps or stays the same depending on what operator we move the scope of the quantifier 'over'. Indeed, it turns out that your equivalence is a bit of an exception: the only time the quantifier gets swapped is if we move it over the consequent of a conditional (or put differently, if the quantifier in the LHS is the antecedent of a conditional).

Finally, I would like to point out that there is not a corresponding Prenex law for biconditionals: there is no easy way to pull a quantifier 'over' a biconditional, and we can understand, given that the quantifier swaps when it is the antecedent of a conditional, but stays the same when it is the consequent. Indeed, if you want to pull out a quantifier when you have a biconditionals, you first have to rewrite the biconditionals as two conditionals, and then apply the two relevant Prenex laws for each of the conditionals (and, of course, pull them over the conjunction between them as well)

Also, the last two Prenex Laws can be derived from the others (actually, from the first two you can derive all others, and same for the third and fourth; this might be a good exercise).

Just doing yours:

$$\exists x \ [P(x)] \rightarrow Q \Leftrightarrow$$

$$\neg \exists x \ [P(x)] \lor Q \Leftrightarrow$$

$$\forall x \ [\neg P(x)] \lor Q \Leftrightarrow$$

$$\forall x \ [\neg P(x) \lor Q] \Leftrightarrow$$

$$\forall x [P(x) \rightarrow Q]$$

You can make some intuitive sense of the Prenex Laws by observing that a universal can be seen as kind of conjunction, and an existential as a kind of existential. That is, if $a,b,c,...$ denote the objects in your domain, then you can think of universals and existentials like this:

$$\forall x \: P(x) \approx P(a) \land P(b) \land P(c) \land ...$$

$$\exists x \: P(x) \approx P(a) \lor P(b) \lor P(c) \lor ...$$

I have to use $\approx$ here, because with different domains you would get different expressions, and so this is certainly not an equivalence! ... but again, intuitively you can make sense of them this way. And ... you can now give an informal proof of your equivalence as well:

$$\exists x \ [P(x)] \rightarrow Q \Leftrightarrow \text{ (Implication)}$$

$$\neg \exists x \ [P(x)] \lor Q \Leftrightarrow \text{ (Quantifier Negation)}$$

$$\forall x \ [\neg P(x)] \lor Q \approx$$

$$(\neg P(a) \land \neg P(b) \land \neg P(c) \land ...) \lor Q \Leftrightarrow \text{ (Distribution)}$$

$$(\neg P(a) \lor Q) \land (\neg P(b) \lor Q) \land (\neg P(c) \lor Q) \land ... \Leftrightarrow \text{ (Implication)}$$

$$(P(a) \rightarrow Q) \land (P(b) \rightarrow Q) \land (P(c) \rightarrow Q) \land ... \approx$$

$$\forall x [P(x) \rightarrow Q] $$

We'll prove the left-hand side implies the right-hand side. Equivalently, combining the LHS with $\exists x [P(x)]$ implies $Q$. Suppose $\exists x [P(x)]$. Fixing that $x$, we get an example of the universal viz. $P(x)\to Q$, so $Q$ as desired.

While we're at it, we'll prove the RHS implies the LHS too (after all, the $\equiv$ claims as much). Suppose $\exists x[P(x)]\to Q$. In particular, any $a$ satisfies $P(a)\to\exists x[P(x)]\to Q$, so $\forall x[P(x)\to Q]$ as claimed.