Getting rid of the set builder notation in the expression $\{ f(x) \mid P(x) \} = \{ g(x)\mid Q(x) \}$

Question

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

Answer 1

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.

Answer 2

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