Call a set-theoretical formula $\phi(x,X)$ a set-builder formula (with parameter $X$) iff $\lbrace x\ |\ \phi(x,X) \rbrace$ is a set for every set $X$.
Call a set-builder formula $\phi(x,X)$ invertible iff there is a set-builder formula $\phi^{-1}(y,Y)$ such that
$$X = \lbrace y\ |\ \phi^{-1}(y,\lbrace x\ |\ \phi(x,X)\rbrace)\rbrace$$
for every set $X$.
Example 1:
$$\phi(\mathbf{x},\mathbf{X}) = \mathbf{x} \in \mathbf{X}$$
Note, that $X = \lbrace x \ |\ \phi(x,X) \rbrace$. Thus $\phi$ can be inverted by
$$\phi^{-1}(\mathbf{y},\mathbf{Y}) = \mathbf{y} \in \mathbf{Y}$$
Example 2:
$$\phi(\mathbf{x},\mathbf{X}) = (\exists z,z')\ \mathbf{x} = (z,z') \wedge z,z' \in \mathbf{X}$$
$Y := \lbrace x \ |\ \phi(x,X) \rbrace$ is the set $X \times X$ of ordered pairs over a given set $X$. $\phi$ can be inverted by
$$\phi^{-1}(\mathbf{y},\mathbf{Y}) = (\exists z,z')\ z =(\mathbf{y},z') \wedge z \in \mathbf{Y}$$
since $X = \lbrace y\ |\ \phi^{-1}(y,Y)\rbrace$ is the underlying set for a given set of ordered pairs $Y$.
Example 3:
$$\phi(\mathbf{x},\mathbf{X}) = (\forall z)\ z \in \mathbf{x} \rightarrow z \in \mathbf{X} $$
$Y := \lbrace x \ |\ \phi(x,X) \rbrace$ is the powerset $P(X)$ of a given set $X$. $\phi$ can be inverted by
$$\phi^{-1}(\mathbf{y},\mathbf{Y}) = (\exists z)\ \mathbf{y} \in z \wedge z \in \mathbf{Y}$$
since $X = \lbrace y\ |\ \phi^{-1}(y,Y)\rbrace$ is the underlying set for a given powerset $Y$.
Counterexample:
$$\phi(\mathbf{x},\mathbf{X}) = (\exists z,z')\ z =(\mathbf{x},z') \wedge z \in \mathbf{X}$$
For arbitrary sets of pairs $X = X_1 \times X_2$ the set $\lbrace x \ |\ \phi(x,X) \rbrace$ equals $X_1$, i.e. is the projection on the first component. Thus $\phi$ cannot be inverted.
Questions
Is the property of being invertible (semi-)decidable for set-builder formulas?
That means, is there a systematic way to tell whether an (invertible) set-builder formula is invertible?
Is a formula $\phi^{-1}$ computable for invertible set-builder formulas $\phi$?
That means, can a formula $\phi^{-1}$ be construed in a systematic way for a given invertible set-builder formula $\phi$?
To ask the first question more softly:
Are there (semi-)obvious necessary and/or sufficient conditions for a set-builder formula to be invertible?