Original proof in the cited forall x natural-deduction system
1. exists x Px          Premise
2. forall x(Px->Qx)     Premise
3. | Pc                 Assumption; c fresh
4. | Pc->Qc             forall E, 2
5. | Qc                 ->E, 3,4
6. | exists x Qx        exists I, 5
7. exists x Qx          exists E, 1, subproof 3-6; discharge Pc
The temporary c occurs in neither premise, the source existential nor the final conclusion.
Countermodel to exists x Px -> Pa: D={A,B}; a denotes A; P={B}; Q={B}.
exists P and forall(P->Q) true; Pa and Qa false; exists Q true.