Moving an Existential quantifier out of an implication using fitch.

Question

I've looked just about every place I could think of and found the necessary rules multiple times, yet no proofs for those derived rules. Most proofs are for conjunctions, yet i have not found any for implications.

An example for such a statement and the corresponding target statement would be:

$\exists xPx\to\exists yPy\therefore\exists y(\exists xPx\to Py)$

I have made multiple attempts with $\to$I and $\neg$E but no luck so far. Can you guys give me a hint?

Answer 1

The hypothesis is a tautology, and thus is of no use in the proof.

From http://proofs.openlogicproject.org/:

Answer 2

Here is a proof done in Fitch: