Much of mathematics is about solving and resolving equations, most prominently algebraic equations. But is there a general theory of resolving set builder equations?
To give an example, the equation
$Y = \{y\ |\ (\exists x,x')\ x,x' \in X \wedge y = (x,x')\}$
defines the set $Y= X \times X$ for a given set $X$. It can be "resolved" by
$X = \{x\ |\ (\exists y,x')\ y \in Y \wedge y =(x,x')\}$
which gives back the underlying set $X$ for a given set of pairs $Y$.
Another example: the equation
$Y = \{y\ |\ (\forall x)\ x \in y \rightarrow x \in X\}$
defines the powerset $Y = P(X)$ for a given set $X$. It can be resolved by
$X = \{x\ |\ (\exists y)\ x \in y \wedge y \in Y \}$
which gives back the underlying set $X$ for a given powerset $Y$.
For which set theoretic formulas such an inverse formula can be construed systematically, and how?