Set-builder notation and predicate logic

Question

I always had trouble translating set-builder notation to predicate logic. When dealing with the most basic examples, all seems pretty straightfoward to me. However, some texts use translations that are not in harmony with my knowledge. So, I'll first cover the cases (I suppose) I understand:

1. $S = \{ x : P(x)\}$ is equivalent to $\forall x[x \in S \leftrightarrow P(x)] $
2. $S = \{ x \in A\}$ is equivalent to $\forall x[x \in S \leftrightarrow x \in A] $
3. $S = \{ x \in A : P(x)\}$ is equivalent to $\forall x[x \in S \leftrightarrow x \in A \space\land P(x)]$

And here I present the cases I'm having a hard time with:

4. [Image of a mapping] $S = \{ y \in Y : \exists x \in A : y = f(x)\}$. Is it equivalent to $\forall x[x \in S \leftrightarrow \forall y[y \in Y \rightarrow \exists x [x \in A \space\land y = f(x)]]$?

5. [taken from the Wikipedia article about Cantor's theorem] $S = \{ x \in A : x \notin f(x)\}$. The article says this is equivalent to $\forall x \in A (x \in S \leftrightarrow x \notin f(x))$. How? For me, it would be: $\forall x[x \in S \leftrightarrow x \in A \space \land x \notin f(x)]$.

Thanks for the help.

Answer 1

As you have written in 3), to write $S = \{ x \in A : P(x) \}$ means that the set $S$ is the subset of $A$ "made of" the elements of $A$ that satisfy condition $P(x)$.

In the same way for 4), the set $S$ is the subset of $Y$ that satisfies the condition to the right of "$:$".

This means: $y \in S \leftrightarrow (y \in Y \land ∃x \in A(y=f(x)))$.

This amounts to saying that $f$ is a function from $A$ to $Y$ and $S$ is the subset of $Y$ made of "images" of elements of $A$, and this is what we expect as "image".

---

The same for 5): $S = \{ x∈A : x∉f(x) \}$.

The set $S$ is made of the elements $x$ of $A$ such that $x \notin f(x)$, i.e.

$x \in S \leftrightarrow (x \in A \land x \notin f(x))$.

An this in turn implies [in fact, it is equivalent to]:

$x \in A \to (x \in S \leftrightarrow x \notin f(x))$.