Is the existence of double complement of a set provable in Intuitionistic ZF?

In Powell's article [1] he introduces the axiom of double complement, which says a double complement $\{x : \lnot\lnot(x\in A)\}$ is a set for any set $A$.

I can't find similar axiom from other references, even in the Friedman's article [2] on double negation over set theories. Hence it is natural to ask the relation between his axiom and other axioms of IZF. (Note: Powell consider the axiom of collection rather than the replacement in his article, but I will consider full IZF.)

I have made some attempts on this problem: if $f(\beta):=\sup\{\alpha\in\mathrm{On} : \lnot\lnot(\alpha<\beta)\}$ exists for each ordinal $\beta$, then the axiom of double complement holds: then $\{x\in V_{f(\operatorname{rank}(A))} : \lnot\lnot(x\in A)\}$ would be the double complement of $A$. (Here $V_\alpha := \bigcup_{\beta\in\alpha} \mathcal{P}(V_\beta)$ is a von Neumann hierarchy. Axiom of power set is necessary in my argument.) However checking $f(\beta)$ is a set is at least as hard as checking the axiom of double complement.

Forcing or realizability seems not helpful to me. This is because we need to generate a set whose double complement is proper class to prove the independence of the axiom of double complement, and it seems to need a proper-class sized name. However both methods just deal with set-sized names.

My question is: Is the axiom of double complement provable from full IZF? If not, is it indenpendent from IZF? Is the axiom of double complement related to the law of excluded middle? I would appreciate any help.

References

[1] Powell, William C. "Extending Gödel's negative interpretation to ZF." The Journal of Symbolic Logic 40.2 (1975): 221-229.

[2] Friedman, Harvey. "The consistency of classical set theory relative to a set theory with intuitionistic logic 1." The Journal of Symbolic Logic 38.2 (1973): 315-319.

A good question. Bear in mind that there can be no set x whose double complement is the universe. (Think about $\{y\in x: y \not\in y\}$). If you are thinking in terms of a cumulative hierarchy picture of constructive sets then what this is trying to tell you is that, for any x, there comes a stage by which all things notnotin x have appeared. And of course, once you have reached such a stage you obtain doublecomp x by separation. But [the rank of] this stage might increase so steeply with the rank of x that no effective proof can be given that there is such a stage. If you pursue this line of thought you will probably be able to come up with a kripke model in which lots of sets lack double complements. I'll have a think about it and get back.