Definable Partition Principle: If $\phi;\psi$ are formulas in which only the symbol $x$ occur free, then: $$A = \{x \mid \phi\} \land B=\{x \mid \psi\} \land B \, ||| \, A \to B \leq A$$ Where $|||$ means “is a partition of“; $B \leq A$ means there exists an injection from $B$ to $A$

Is this provable in ZF? If not, is it equivalent to AC over ZF?