Getting rid of the set builder notation in the expression $\{ f(x) \mid P(x) \} = \{ g(x)\mid Q(x) \}$ The set-builer notation is used to have   
$$\{ x \mid P(x) \} = \{ x \mid Q(x) \}$$
denote   
$$\forall x\ \big(P(x) \Leftrightarrow Q(x) \big).$$
And some people write   
$$\{ x \in U \mid P(x) \} = \{ x \in U \mid Q(x) \}$$
to denote   
$$\forall x\ \big( x \in U \Rightarrow (P(x) \Leftrightarrow Q(x)) \big).$$
Now I want to translate the frequently used
$$\{ f(x) \mid P(x) \} = \{ g(x) \mid Q(x) \}$$
where the elements are not $x$, but sets constructed from them via $f$ and $g$. My try is
$$\forall y\ \big(\exists x\ \big(y=f(x)\land P(x)) \Leftrightarrow \exists x'\ \big(y=g(x')\land Q(x')\big) \big)$$
but I'm e.g. not sure about the existential quantifiert, or if I really need two. 
I figure a necessary condition for having found the right way would be to try $f=g=\text{id}$ and see the formula reducing to the previous expression. However, I fail at this, because I don't know how to unpack it. I think I'd have to use $y=x$ and $y=x'$, but I don't know how I'd formally get this statement out of the long formula, so that I can use it?

What is the right way to read $\{ f(x) \mid P(x) \} = \{ g(x) \mid Q(x) \}$ and how to show it reduces to $\forall x\ \big(P(x) \Leftrightarrow Q(x) \big)$ for $f=g=\text{id}$?


Your translation is correct.  To unpack the specialization to $f=g=\text{id}$, use the fact (of logic) that $\exists x\,(y=x\land P(x))$ is equivalent to $P(y)$.
