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

-
I didn't read everything, but hopefully this will help: $\{f(x)|P(x)\}$ should be read as $$\{y|\bigl(\exists x\in \text{dom}(f)\bigr)(f(x)=y)\land P(x)\}.$$ Related. – Git Gud Jun 8 '13 at 19:39

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)$.