$\newcommand{\abs}[1]{\left\lvert #1 \right\rvert}$ $\newcommand{\powerset}[1]{\mathcal{P}\left(#1\right)}$ $\newcommand{\realset}{\mathbb{R}}$
I am using the Heine-Borel theorem to prove the following proposition: if a function $f$ is continuous on a compact interval $I$, then $f$ is uniformly continuous on $I$. I doubted if it is legitimate to assert the existence of a function at the start of the proof.
The Heine-Borel theorem states that if $\mathcal{H}$ is an open covering for a compact set $I$, then there is a $\widetilde{\mathcal{H}}$ such that $\widetilde{\mathcal{H}} \approx n$ for some $n \in \mathbb{N}$ and $\widetilde{\mathcal{H}} \subseteq \mathcal{H}$ and $\widetilde{\mathcal{H}}$ is an open covering of $I$. Below is the starting point of the proof.
Suppose $\epsilon_{0} > 0$ and $t_{0} \in \left[a,b\right]$. Since $f$ is continuous on $\left[a,b\right]$, there exists some $\delta_{0}$ such that if $x_{0} \in \left(t_{0} - 2\delta_{0}, t_{0} + 2\delta_{0}\right) \cap \left[a,b\right]$, then \begin{equation} \abs{f\left(x_{0}\right) - f\left(t_{0}\right)} < \frac{\epsilon_{0}}{2} \end{equation} Generalizing the above statement, for any $\epsilon > 0$, for any $t \in \left[a,b\right]$, there exists some $\delta > 0$ such that for any $x \in \left(t - 2\delta,t + 2\delta\right) \cap \left[a,b\right]$, $\abs{f\left(x\right) - f\left(t\right)} < \epsilon / 2$. Thus, there exists an interval function $I: \left[a,b\right] \to \powerset{\realset}$ defined on $\left[a,b\right]$ such that for any $t \in \left[a,b\right]$, there exists $\delta_{t} > 0$ such that \begin{equation} I_{t} = \left(t - \delta_{t}, t + \delta_{t}\right), \end{equation} and for any $\epsilon > 0$, for any $x \in I_{t} \cap \left[a,b\right]$, $\abs{f\left(x\right) - f\left(t\right)} < \epsilon / 2$, and \begin{equation} \left[a,b\right] \subseteq \bigcup_{t\in\left[a,b\right]}I_{t}. \end{equation}
I am a little skeptical about the existence of function $I$, as there exists such an interval $I_{t}$ for any $t\in \left[a,b\right]$ does not mean the function $I$ exists. It seems to me that the argument is related to axiom of choice in set theory, as the axiom is introduced with the background that construction of function is needed when there exists an object for every point of a set while the object cannot be uniquely determined. Is it also a scenario where axiom of choice is needed to argue the existence of such a function?
The axiom of choice is not needed here. While it is true that in general to go from "$\forall \mathcal{X}\exists \mathcal{Y}\theta(\mathcal{X},\mathcal{Y})$" to "$\exists\mathscr{F}\forall\mathcal{X}\theta(\mathcal{X},\mathscr{F}(\mathcal{X}))$" we need the axiom of choice, we rarely in practice actually need to appeal to this general principle.
In this case, note that $I$ is in fact determined by the function $t\mapsto\delta_t$; moreover, there's no reason not to have each $\delta_t$ be a positive rational. Now we can fix ahead of time a well-ordering $\trianglelefteq$ of the positive rationals, and consider the explicitly-defined function sending $t$ to the $\trianglelefteq$-least positive rational with the appropriate properties. This doesn't require choice at all.
(In general, arguments in classical analysis tend not to require choice due to the second-countability of $\mathbb{R}$.)