I hope this question isn't too obfuscated (or easy)!

Given a set $S$, let $S_\perp$ denote $\{X \in \mathcal P(S) \mid \forall x, y \in X.\, x=y\}$, the elements of which are *subsingletons*. In the following $Y_\perp^X$ means $(Y_\perp)^X$.

The question is: *does a partial map between $X$ and $Y$ that doesn't have $\emptyset$ in its image determine a subsingleton of maps between $X$ and $Y$ which is non-empty?*

The same thing written more accurately with symbols: Assume that we have an element $F$ of $Y_\perp^X$ that doesn't have $\emptyset$ in its image. Can we conclude that there exists an element $F'$ of $(Y^X)_\perp$ such that $F' \neq \emptyset$ and $\forall f' \in F'.\,\forall x \in X.\,f'(x) \in F(x)$?

In the presence of Excluded Middle, this question is easy. In its absence, it seems much harder.

**This is my main lead right now:**

We assume the the Axiom of Unique Choice.

We need to prove that $$\begin{align} \forall x\in X. (\forall y, y'. \phi(x,y) \wedge \phi(x,y') \implies y=y') \wedge (\neg\neg\exists y \in Y. \phi(x,y)) \tag{1} \end{align}$$ implies $$\begin{align} \neg\neg \exists f \in Y^X. \phi(x,f(x)). \tag 2 \end{align}$$

We can use the fact that $p \implies q$ implies $\neg\neg p \implies \neg\neg q$, and the Principle of Unique Choice. The calculations seem quite difficult. We would need to get (1) into the form $$\begin{align} \neg\neg(\forall x\in X. (\forall y, y'. \phi(x,y) \wedge \phi(x,y') \implies y=y') \wedge \exists y \in Y. \phi(x,y)) \tag{1'} \end{align}$$