Under Dependent Choice, every completely metrizable subspace of a metric space is $G_{\delta }$

The empty subspace is the constant countable intersection of the ambient open set $\mathrm{\varnothing }$.

Let $\rho$ be a compatible complete metric on the nonempty subspace $Y$ and let $d$ be the ambient metric. For $n\ge 1$ call an ambient open $V$ $n$-small when $V\cap Y\mathrm{\ne }\mathrm{\varnothing }$, ${\mathrm{diam}}_d(V)<1\mathrm{/}n$, and ${\mathrm{diam}}_{\rho }(V\cap Y)<1\mathrm{/}n$. Both conditions are imposed, and neither may be dropped: $\rho$-smallness alone controls distances measured in $\rho$ but says nothing about ambient distances, so it cannot force a point of $Y$ to be near a prescribed ambient point, while ambient smallness alone gives no $\rho$-control and so cannot invoke completeness of $\rho$. Every $y\in Y$ lies in some $n$-small $V$, because $\rho$ induces the subspace topology, so a $\rho$-ball of radius below $1\mathrm{/}2n$ about $y$ contains $B_d(y,r)\cap Y$ for some $r>0$, and $r$ may be shrunk below $1\mathrm{/}2n$. Let $G_n$ be the union of all $n$-small ambient open sets, an ambient open set containing $Y$.

Every $x\in {\bigcap }_{n\ge 1}{G}_n$ lies in $\bar{Y}$. [step 2.1, F5] Indeed, given $r>0$, choose $n\ge 1$ with $1\mathrm{/}n<r$. There is an $n$-small open $V$ containing $x$, and some $y\in V\cap Y$. Then $d(x,y)<1\mathrm{/}n<r$. Thus every ambient ball about $x$ meets $Y$. This uses only finitely many choices for each fixed $r$, not a selected sequence.

Let $x\in \bar{Y}\cap {\bigcap }_{n\ge 1}{G}_n$. For each $n$ pick an $n$-small $V_n$ with $x\in V_n$ and put $W_n:=V_1\cap \cdots \cap V_n$, an ambient open neighbourhood of $x$ with $W_n\subseteq V_n$, so ${\mathrm{diam}}_d(W_n)<1\mathrm{/}n$ and ${\mathrm{diam}}_{\rho }(W_n\cap Y)<1\mathrm{/}n$; the $W_n$ decrease. Then pick $y_n\in W_n\cap Y$, which is nonempty because $x\in \bar{Y}$ and $W_n$ is an ambient neighbourhood of $x$. The selection over $n$ is a recursion whose $n$th admissible set depends on the previous choices, so it is licensed by the Dependent Choice of [F3]. Since $x,y_n\in W_n$ and ${\mathrm{diam}}_d(W_n)<1\mathrm{/}n$, the points $y_n$ converge to $x$ in $d$. For $m,n\ge N$ both $y_m$ and $y_n$ lie in $W_N\cap Y$, so $\rho (y_m,y_n)<1\mathrm{/}N$ and the sequence is $\rho$-Cauchy; completeness of $\rho$ gives it a $\rho$-limit in $Y$.

Let $y\in Y$ be the $\rho$-limit from step 3.2. [step 3.2, F4, F1] The compatible topologies make $y_n$ converge to $y$ in the subspace $d$-metric, hence in $X$. It also converges to $x$. If $x\mathrm{\ne }y$, disjoint open neighbourhoods from [F4] would both contain every sufficiently late $y_n$, a contradiction. Hence $x=y\in Y$.

Therefore $Y={\bigcap }_{n\ge 1}{G}_n$. [step 2.1, step 3.1, step 4.1, F2] Reindexing by $n+1$ gives a sequence indexed from zero as in [F2], so $Y$ is $G_{\delta }$ in $X$. The only countable selection is the stated DC use in step 3.2; the empty case was handled in step 1.1. ∎