I need help proving $\exists x:[D(x)\implies Q]$ for arbitrary unary predicate $D$ and proposition $Q$.
I think it should be possible since I have been able to prove a set-theoretic version: $\exists x: [x\in D \implies Q]$ for arbitrary set $D$ and proposition $Q$, but I don't see how to translate it into a purely FOL proof.
On further consideration, the FOL version is clearly not true in general. Consider, for example, the case of $\forall x: D(x)$ being true and $Q$ being false.
The set-theoretic version, however, is obviously true if the universal set does not exist. Since every set would then exclude something, we must then have some $x$ such that $x\notin D$. Introducing disjunction, we have $x\notin D \lor Q$ or equivalently $x\in D \implies Q$. Generalizing, we have $\exists x:[x\in D\implies Q]$.
The two, seemingly equivalent statements are at odds with one another. Is this not a problematic?
It is not problematic at all. You simply have more ways to prove things, more tools with set theory. In set theory, you can construct subsets and quantify over sets. Both of these tools are essential to the resolution of the Paradox of the Universal Set, which in turn is essential to prove $\exists x:[x\in D\implies Q]$. There is no equivalent of these tools available in FOL. This leaves $\exists x:[D(x)\implies Q]$ unprovable in FOL.