There is a common view amongst mathematicians that uses of the axiom of choice must somehow be inherently undefinable, and that if one sticks with definable sets only, then everything will be very nicely behaved.
The question here is an instance of this perspective, since it is asking whether every definable set of reals must be Borel.
But unfortunately, the view is simply mistaken. One way to see this is to observe that the constructible universe L of Gödel has a definable well ordering of the set-theoretic universe. Thus, in $L$ all uses of the axiom of choice can be undertaken in a definable manner, since one can always make the choices by picking the least element with respect to the definable well order.
For example, in $L$ there is an $L$-least non-Borel set. So we can take $Px$ to assert: $x$ is the least non-Borel set in $L$, using the definable $L$-order. This defines a unique set in any model of set theory, a set of reals, and ZF cannot prove that it is Borel, because it is not Borel if $V=L$. But it could be Borel in other models of set theory, since by forcing we can make every set of reals in $L$ countable and hence Borel.
Similarly, Asaf mentions another example in his comment, namely, the set of reals of the constructible universe $\newcommand\R{\mathbb{R}}\R^L$. This is definable in $V$, but it is consistent that this set is not Borel. This definition has very low complexity in the descriptive set-theoretic hierarchy, $\Sigma^1_2$. That is, it is defined by a formula of the form $\exists y\in\R\forall z\in\R\ \varphi(x,y,z)$, where the quantifiers range over $\R$ and $\varphi$ involves only quantification over integers.
More generally, any set at all can become definable in a forcing extension of the universe. Indeed, there is a single definition $P$, such that for any model of set theory $M$ and any object $a\in M$, there is a forcing extension $M[G]$ in which $P$ defines $a$ in $M[G]$. For example, let $Px$ hold when $x$ is the set coded (in one of the canonical manners) by the class of ordinals defined by the GCH pattern on the regular cardinals, with some default value if the coding fails. Since by Easton's theorem we can control the GCH pattern as we wish on the regular cardinals, we can use this method to make any desired set definable by this same definition. And we can arrange the forcing to not add reals or sets of reals, so the concept of Borel will be the same in $M$ as in $M[G]$.
Another universal definition arises with the Universal finite set and its generalization to The universal $\Sigma_1$ definition, which shows how to make any set you like definable on the universal finite sequence.
Thus, there is no necessary implication from definable-in-ZF to always-having-nice-regularity-properties. Even badly behaved sets can be definable, and indeed, any set at all can become definable.
