How to prove $\forall x:P(x) \implies \exists x:P(x)$ without using UI? In standard FOL, can we prove $\forall x: P(x) \implies \exists x:P(x)$ without introducing a new free variable by universal instantiation, i.e without using $\forall x: P(x) \vdash P(y)$ where $y$ is not does not occur in $P(x)$? 
I have tried direct proof, proof by contradiction, and proof by contrapositive. It looks impossible to me, but can't prove it.

If you use the following system from A Primer for Logic and Proof, Holly P. Hirst and Jeffry L. Hirst, 

Axioms 
  Axiom 1: $A \implies (B \implies A)$ 
  Axiom 2: $(A \implies (B \implies C)) \implies ((A \implies B) \implies (A \implies C))$ 
  Axiom 3: $(\lnot B \implies \lnot A) \implies ((\lnot B \implies A) \implies B)$ 
  Axiom 4: $(\forall x ~:~  A(x)) \implies A(t)$, provided that $t$ is free for $x$ in $A(x)$. 
  Axiom 5: $\forall x ~:~ (A \implies B) \implies (A \implies \forall x ~:~ B)$, provided that $x$ does not occur free
  in $A$. 

  Rules of inference 
  Modus Ponens (MP): From $A$ and $A \implies B$, deduce $B$. 
  Generalization (GEN):  From $A$, deduce $\forall x ~:~ A$. 

Notice that axiom 4 is the only axiom that doesn't hold in an empty universe (substitute false for A).  Also notice the theorem to prove doesn't hold in an empty universe.  So this axiom must be used somewhere in the proof.  So a new variable must be introduced if you use these axioms.
