# Resolving set builder equations

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?

-