Question on set-builder notation Wikipedia's article on set-builder notation explains that the set $\{f(x) : P(x)\}$ is equal to $\{y : \exists x [y=f(x) \land P(x)]\}$. As far as I understood, $S = \{f(x) : P(x)\}$ can be expressed in predicate logic as $\forall x[f(x) \in S \leftrightarrow P(x)]$, while $S = \{y : \exists x [y=f(x) \land P(x)]\}$ can be written as $\forall y [y \in S \leftrightarrow \exists x[y=f(x) \land P(x)]]$. However, these two formulas are logically equivalent, only if the function $f$ is invertible. Is that correct?
 A: It is true that, in general (that is, for a generic function $f$), the sentences
\begin{align}\tag{1}
\forall x \, [f(x) \in S &\leftrightarrow P(x)] 
\\
\tag{2}
\forall y \, [y \in S &\leftrightarrow \exists x [y = f(x) \land P(x)]]
\end{align}
are not logically equivalent. More precisely:

*

*$(1)$ does not imply $(2)$, but the implication holds if the function $f$ is surjective in $S$ (i.e. $S$ is included in the image of $f$).

*$(2)$ does not imply $(1)$, but the implication holds if the function $f$ is injective in $S$ (i.e. for all $x$ and $x'$ in the domain of $f$, if $f(x) = f(x') \in S$ then $x = x'$);

The sentences $(1)$ and $(2)$ are logically equivalent if the function $f$ is invertible in $S$ (i.e. injective in $S$ and surjective in $S$). But it is still possible, a priori, that for some function $f$ non-invertible in $S$, $(1)$ and $(2)$ are equivalent.

However, the point is that the definition $S = \{f(x) : P(x)\}$ is not expressed in predicate logic by  means of $(1)$, but only by means of $(2)$.
Indeed, setting $S = \{f(x) : P(x)\}$ (or equivalently, $S = \{y : \exists x \, [y = f(x) \land P(x)]\}$) means that the elements of $S$ are all and only the images via $f$ of the points with the property $P$.
Why does the sentence $(1)$ not mean that $S = \{f(x) : P(x)\}$?
First, the sentence $(1)$ does not say anything about the elements of $S$ that are not of the form $f(x)$, hence $(1)$ does not exclude the possibility that $S$ can have some elements that are not in the image of the function $f$. But the definition $S = \{f(x) : P(x)\}$ and the sentence $(2)$ do exclude this possibility.
Note that that possibility is excluded whenever $f$ is surjective in $S$, that is, when $S$ is a subset of the image of $f$: this is the reason why $(1)$ implies $(2)$ when $f$ is surjective in $S$.
Moreover, the sentence $(2)$ and the definition $S = \{f(x) : P(x)\}$ do not exclude the possibility that $P(x')$ holds but $P(x)$ does not, for some $x \neq x'$ with $f(x) = f(x')$; hence, in that case $f(x) \in S$ (because $f(x) = f(x')$ and $P(x')$ holds) but $P(x)$ does not hold. But the sentence $(1)$ do exclude this possibility.
Note that that possibility is excluded whenever $f$ is injective in $S$, that is, when every element in $S$ is the image via $f$ of at most one point in the domain of $f$: this is the reason why $(2)$ implies $(1)$ when $f$ is injective in $S$.
Summing up, defining $S = \{y : \exists x \, [y = f(x) \land P(x)]\}$ (or equivalently $S = \{f(x) : P(x)\}$, which is just a shorter notation of the same definition) means what is expressed by $(2)$.
