The unit interval with its Borel structure is standard Borel

The interval is closed in $\mathbb{R}$: for $z\mathrm{\notin }I$, [F6] and [A1] give either $z<0$ or $z>1$. If $z<0$, set $r=-z>0$; then every $y\in B(z,r)$ satisfies $y<z+r=0$. If $z>1$, set $r=z-1>0$; then every $y\in B(z,r)$ satisfies $y>z-r=1$. By [F1] these are open neighborhoods disjoint from $I$, so its complement is open by [F10]. Thus $I$ is Borel by [F7].

The set $D:=\mathbb{Q}\cap I$ is at most countable: restrict the bijection $\mathbb{Q}\to \mathbb{N}$ from [F3] to $D$, then apply [F5]. It is dense in $I$. Indeed, for $x\in I$ and $\epsilon >0$, if $x=1$ choose $q=1$. If $x<1$, then $x+\epsilon >x$; take $b=x+\epsilon$ when $x+\epsilon \le 1$, and $b=1$ otherwise. In either case $b>x$ and $b-x\le \epsilon$, with strict inequality in the second case. By [F4] choose a rational $q$ with $x<q<b$; then $q\in D$ and $\mathrm{\mid }q-x\mathrm{\mid }<\epsilon$. The order comparisons use [F6] and the interval endpoints use [A1].

Let $(x_n)$ be a Cauchy sequence in $I$ under $d_I$. By [A2]–[A3], Cauchy distances are the same in $I$ and $\mathbb{R}$, so [F2] gives a real limit $x$. If $x\mathrm{\notin }I$, step 1.1 gives an open ball about $x$ disjoint from $I$, while convergence puts all sufficiently late $x_n$ in that ball, a contradiction. Hence $x\in I$ and the sequence converges in the restricted metric; $(I,d_I)$ is complete.

By steps 1.2 and 2.1, $I$ is separable and completely metrizable, hence Polish by [F9]. Its Borel sigma-algebra is the trace of $\mathcal{B}(\mathbb{R})$ by [F8] and [A2]. The identity map from $(I,\mathcal{B}(\mathbb{R}){\mathrm{\mid }}_I)$ to the Polish subspace $I$ is therefore a bimeasurable bijection; [F9] makes $(I,\mathcal{B}(I))$ standard Borel. This proves the claim without any choice axiom.