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}$?

 A: 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)$.
A: 
I want to translate

$$\{ f(x) \mid P(x) \} = \{ g(x) \mid Q(x) \}\tag1$$

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)\tag2$$

I obtained the same formalisation.
In Prenex form (verification): \begin{gather} ∀y\:∀a\:∀b\:∃c\:∃d\: \bigg(  \Big(y{=}f(a)∧P(a) \Big) ∨ \Big(y{=}g(b)∧Q(b) \Big) \\
 → y{=}f(c)∧y{=}g(d)∧P(c)∧Q(d)  \bigg).\tag3\end{gather}

how to show it reduces to $\forall x\ \big(P(x) \Leftrightarrow Q(x) \big)$ for $f=g=\text{id}$?

Setting the $f$ and $g$ in $(3)$ as the identity function:
\begin{align}&∀y\:∀a\:∀b\:∃c\:∃d\: \bigg(  \Big(y=a∧P(a) \Big) ∨ \Big(y=b∧Q(b) \Big) \\
& → y=c∧y=d∧P(c)∧Q(d)  \bigg)\\
\equiv{}&∀y\: \bigg(  ∃a\:\Big(y=a∧P(a) \Big) ∨ ∃b\:\Big(y=b∧Q(b) \Big) \\
& → ∃c\:\Big(y=c∧P(c)\Big) ∧ ∃d\:\Big(y=d∧Q(d)\Big)\bigg)\\
\equiv{}&∀y\: \bigg(  P(y)  ∨ Q(y)  → P(y) ∧ Q(y)\bigg) \\
\equiv{}&∀y\:  \bigg( \big(\lnot P(y)  ∧  \lnot Q(y) \big)  ∨  \big( P(y)∧Q(y) \big) \bigg) \\
\equiv{}&∀y\:  \Big(  P(y) \leftrightarrow Q(y) \Big) \\
\equiv{}&∀x\:  \Big(  P(x) \leftrightarrow Q(x) \Big), \end{align}
where the second logical equivalence appeals to Andreas's suggestion $$\exists x\,(y=x\land P(x)) \quad\equiv\quad \exists x\,(P(y)) \quad\equiv\quad P(y),$$ which when plugged into $(2)$ directly gives the same result.
