I've been trying it in Joachim Breitner's fun little Incredible Proof Machine applet (https://incredible.pm/), mostly just because it's easy to visualize that way, but I don't think that's essential. The applet does basicall constructive logic (with not $\lnot P$ represented as $P \Rightarrow \bot$) and an excluded middle axiom if you want to do classical logic.
I can prove the constructively valid direction $$ \cfrac{\cfrac{\cfrac{\exists x. P(x)} {P(k)} \cfrac{[\forall x. \lnot P(x)]} {\lnot P(k)}} {\bot}} {\lnot \forall x. \lnot P(x)}$$ but I can't do it the other way around. I know I need the LEM axiom since it's only classically valid, but I'm not sure where to put it or what to instantiate it with.
$\def\fitch#1#2{~~~~\begin{array}{|l} #1\\\hline #2\end{array}}$ Note: Well, you do not need the LEM axiom, @Zyzzyva, since Double Negation Elimination is equally non-constructive. Though you may use it if you so desire. Every LEM proof has an equivalent RAA proof.
The key point is that if you assume that there is no such entity that satisfies $P$, then any arbitrary entity must satisfy $\neg P~$ (IE: $\neg\exists x~P(x)\vdash \forall x~\neg P(x)$) . This would contradict a prior assumption for the desired conditional proof.
$$\begin{split}P(k)&\vdash \exists x~P(x)&\text{existential introduction}\\\neg\exists x~P(x),P(k)&\vdash\bot&\text{negation elimination}\\\neg\exists x~P(x)&\vdash\neg P(k)&\text{negation introduction}&(4)\\\neg\exists x~P(x)&\vdash\forall x~P(x)&\text{universal introduction}&(3)\\\neg\forall x~\neg P(x),\neg\exists x~P(x)&\vdash\bot&\text{negation elimination}\\\neg\forall x~\neg P(x)&\vdash\neg\neg\exists x~P(x)&\text{negation introduction}&(2)\\\neg\forall x~\neg P(x)&\vdash\exists x~P(x)&\text{double negation elimination}\\&\vdash \neg\forall x~\neg P(x)\to\exists x~P(x)\quad&\text{conditional introduction}\quad&(1)\end{split}$$
As you see, we raise and discharge four assumptions: $\neg\forall x~\neg P(x), \neg\exists x~P(x),$ arbitrary variable $k$, and $P(k)$. (Although some systems do not explicitly describe a local variable as an "assumption", its context is raised and discharged.)
The LEM proof is easily built from this:
$$\begin{split}&\vdash(\exists x~P(x))\vee(\neg\exists x~P(x))&\text{law of excluded middle}\\[1ex]\exists x~P(x)&\vdash\exists x~P(x)&\text{reiteration}\\[1ex]P(k)&\vdash \exists x~P(x)&\text{existential introduction}\\\neg\exists x~P(x),P(k)&\vdash\bot&\text{negation elimination}\\\neg\exists x~P(x)&\vdash\neg P(k)&\text{negation introduction}&(5)\\\neg\exists x~P(x)&\vdash\forall x~P(x)&\text{universal introduction}&(4)\\\neg\forall x~\neg P(x),\neg\exists x~P(x)&\vdash\bot&\text{negation elimination}\\\neg\forall x~\neg P(x),\neg\exists x~P(x)&\vdash\exists x~P(x)&\text{explosion}\\\hline\neg\forall x~\neg P(x)&\vdash\exists x~P(x)&\text{disjunction elimination}&(2,3)\\&\vdash \neg\forall x~\neg P(x)\to\exists x~P(x)\quad&\text{conditional introduction}\quad&(1)\end{split}$$
That just leaves translating it into your preferred format.
$$\phantom{\tiny{\dfrac{\dfrac{\dfrac{\dfrac{\lower{1.5ex}{[\neg\forall x~P(x)]^1}~\dfrac{{\dfrac{\dfrac{\lower{1.5ex}{[\neg\exists x~P(x)]^2}~\dfrac{[P(k)]^4}{\exists x~P(x)}{\tiny\exists\mathsf I}}{\bot}{\tiny\neg\mathsf E}}{\neg P(k)}{\tiny\neg\mathsf I^4}}}{\forall x~\neg P(x)}{{\tiny\forall\mathsf I}^{\small\require{cancel}\cancel k}}}{\bot}{\tiny\neg\mathsf E}}{\neg\neg\exists x~P(x)}{\tiny\neg\mathsf I^2}}{\exists x~P(x)}{\tiny\neg\neg\mathsf E}}{\neg\forall x~\neg P(x)\to\exists x~P(x)}{\tiny\to\mathsf I^1}}\tiny{\dfrac{\dfrac{\dfrac{}{\left(\exists x~P(x)\right)\vee\left(\neg\exists x~P(x)\right)}{\tiny\textsf{LEM}}~\dfrac{[\exists x~P(x)]^2}{\exists x~P(x)}{\tiny\mathsf{R}}~\dfrac{\dfrac{\lower{1.5ex}{[\neg\forall x~P(x)]^1}~\dfrac{{\dfrac{\dfrac{\lower{1.5ex}{[\neg\exists x~P(x)]^3}~\dfrac{[P(k)]^5}{\exists x~P(x)}{\tiny\exists\mathsf I}}{\bot}{\tiny\neg\mathsf E}}{\neg P(k)}{\tiny\neg\mathsf I^5}}}{\forall x~\neg P(x)}{{\tiny\forall\mathsf I}^{\small\require{cancel}\cancel k}}}{\bot}{\tiny\neg\mathsf E}}{\exists x~P(x)}{\tiny\mathsf X}}{\exists x~P(x)}{\tiny\vee\mathsf E^{2,3}}}{\neg\forall x~\neg P(x)\to\exists x~P(x)}{\tiny\to\mathsf I^1}}}$$