It has been pointed out in the comments that Ewan's insightful solution shows that a negative answer to the question is consistent with ZF, since a positive answer implies AC.

But let me go one further. In fact, Ewan's solution shows that a negative answer to the main question is consistent with full ZFC. The reason is that a positive answer to Ewan's problem 2 actually implies the set-theoretic assertion $V=HOD$, that the universe consists of the hereditarily-ordinal-definable sets. To see this, supoose that $V\neq HOD$, then there is some cardinal $\kappa$ such that $Y=P(\kappa)$ has some non-ordinal definable elements. Let $Y'$ be the set of non-HOD subsets of $\kappa$. Both $Y$ and $Y'$ are ordinal definable, but $Y'$ has no ordinal definable elements. This contradicts any positive solution to problem 2.

Thus, any model of set theory having a positive answer to problem 2 must also satisfy $V=HOD$. And so any model of $ZFC+V\neq HOD$ is a model of a negative answer to the main question, with full ZFC.

Meanwhile, a positive answer to the main question is also consistent with ZFC, since there are models of ZFC in which every object is definable without parameters. For example, this is true in the minimal transitive model of set theory. Indeed, Reitz and Linetsky and I have recently proved that every countable model of ZFC and indeed of GBC can be extended to a pointwise definable model, in which every set and class whatsoever is definable without parameters. In such a model, we may definably find the desired B, since every B is definable. (But there is little uniformity in this definition.)

So the full answer to the main question is that it is independent of ZFC. Of course, the question of "definable" is not directly formalizable in set theory, so one should understand this assertion as the claim that if ZFC is consistent, then there are models of ZFC in which there is a positive solution, and models in which there is a negative solution, even when interpreted as the literal second-order claim. However, if one understands "definable" as "ordinal-definable", then the claim is formalizable in the language of set theory, and this claim is also independent of ZFC, for the same reasons.

notrequiring $B$ to be first order definable on $({\mathcal P}(X)\sqcup X,\subseteq, F)$, simply to be definable from $F$ in the language of set theory; this is a much more generous notion of definability. $\endgroup$