What examples of fragments of ZF are consistent with: $$\exists x \exists f\, (f\colon x \to P(x) \wedge f \text{ is bijective})$$ and are not too weak, ideally with at least the consistency strength of PA?

The fragment that I know of is the theory axiomatized by Extensionality, Singletons, Boolean union, Power, Predicative stratified instances of Separation, and Infinity (in the form $\exists x\, (x \text{ is infinite})$)

Another theory has the same axioms above plus set union, but with separation restricted to stratified formulas with three types.

Another theory has all the above axioms and allows all stratified instances of separation, but asserts Extensionality only for non-empty objects. This theory is not known to prove a set that is equal to its power in size, but is consistent with all types of inequality of size between a set and its power. The references for this are known to people working with NF(U).

What other known fragments of ZF are not too weak, and yet are consistent with a set being equal to its power set in size?

`\text`

as a wrapper for when you want text inside a math environment $\endgroup$ – David Roberts Aug 23 '18 at 22:29