The answer follows from an application of some descriptive set theory and Shoenfield's absoluteness theorem. The rest of this answer works the same way in $\mathbb{R}^k$ as in $\mathbb{R}$, but I will write it up (shortly) in $\mathbb{R}$ for notational simplicity.
Actually, the principle in question is a variant of the Baire category theorem and would be provable in a very weak subsystem of second-order arithmetic, even if generalized to an arbitrary complete separable metric space. Second-order arithmetic is much much weaker than ZF. So showing that the principle is provable in ZF is much easier, although I am going to just use the big hammer of Shoenfield's absoluteness theorem here.
Here is a sketch in ZF, showing how to apply the absoluteness theorem. The key point is that we have to show that the principle of interest can be expressed by a formula at a low level of the analytical hierarchy.
Note that given any open set $U$, ZF can form the set $A(U) = \{ (i,j) : B(q_i, 2^{-j}) \subseteq U\}$ where $(q_i)$ is some fixed enumeration of the rational points and $B(\cdot,\cdot)$ denotes a ball as usual. And this construction is uniform; given a sequence $(U_i)$, ZF is able to form $(A(U_i))$.
Furthermore, a set is by definition closed if and only if its complement is open.
Thus, in ZF, the statement that the union of a sequence $(C_k)$ of closed sets covers all of $\mathbb{R}$ can be written in the following form:
$ (\forall x \in \mathbb{R})(\exists i, j,k \in\omega)[ (i,j) \in A(U_k) \land d(x, q_i) < 2^{-j}]. $ where $(U_k)$ is the sequence of the open sets complementary to the sets in thbe sequence $(C_k)$.
The displayed formula is at level $\Pi^1_1$ of the analytical hierarchy if $(A(U_k))$ and the distance function are taken as parameters (the parameters can be taken to be elements of $\omega^\omega$ with routine coding, and the quantifier over $\mathbb{R}$ can be replaced with a quantifier over $\omega^\omega$ with routine methods, and the correctness of these methods can be verified in ZF).
Similarly, the statement that some $C_k$ has nonempty interior can be written as
$ (\exists k)(\forall x\in \mathbb{R})(\exists i,j)[ d(x, q_i) < 2^{-j} \to x \in C_k] $
This is again $\Pi^1_1$ in the analytical hierarchy because we can replace $x \in C_k$ with $x \not \in A(U_k)$ as above. Thus the overall statement "if $\mathbb{R} = \bigcup C_k$ then some $C_k$ has nonempty interior" can be taken, in ZF, to be of the form $(\Pi^1_1) \to (\Pi^1_1)$, and hence this statement is $\Sigma^1_2$ relative to some parameters in $\omega^\omega$.
Shoenfield's absoluteness theorem, which is provable in ZF, states that $\Sigma^1_2$ sentences of the analytical hierarchy with parameters $X \in \omega^\omega$ are absolute - have the same truth value - between $V$ and $L(X)$. Because $L(X)$ provably satisfies ZFC, and ZFC proves the principle in question, ZF can prove that the principle will be true in $L(X)$ and thus also true in $V$ by Shenfield's theorem.