I am struggling to understand how one converts a set written using the set-builder notation to elementary predicate logic. Just for you to have an idea of my background, I studied engineering in college, and I used "high-level" maths (high level in the informatics sense, i.e. without digging to deep in the meaning of what I was writing) and I decided to start learning about ZFC for its own sake. I have no trouble understanding and manipulating sets written using predicate logic, but whenever a set-builder notation pops, I become lost because I am unable to go back to pure logic.
For simple cases such as $S = \{x|x\in A\}$, I clearly understand that it can be translated to ${\forall x(x \in S \leftrightarrow x \in A)}$.
I really started to realize that I did not understood this notation when solving an exercise involving $\{dom R | R \in A\}$. The mistake I made was that I was translating $x\in\{dom R | R \in A\}$ by $\exists y (x,y)\in R$ which is obviously wrong since $x$ should be a domain and not an element of a domain.
Although I am not sure of this, I would expect the solution to be something like $x=dom R \wedge R \in A$.
After this long introduction, my question is pretty simple: how do I turn ANY set written using the set-builder notation, even a complicated one, to a predicate logic formula?
Thanks in advance!
The tricky aspect of the set-builder notation is that it includes an implicit existential quantification for all variables that occur freely within the set formula and are not bound outside of the set formula.
Example: Consider the following sentence: Let $R \in \mathbb{N} \times \mathbb{N}$, let $n \in \mathbb{N}$, let $M = \{z^n \mid \forall w. (z,w) \in R\}$. The variable $w$ is bound by the explicit quantifier within the set-builder notation, the variables $R$, $n$, and $z$ occur freely within the set-builder notation, but $R$ and $n$ are bound outside of the set-builder notation (by the phrase "Let $R \in \mathbb{N} \times \mathbb{N}$, let $n \in \mathbb{N}$"). The usual convention is that all free variables within the set-builder notation that are not bound outside are considered as existentially quantified. In this example, that's $z$, so we get $$x \in M \Leftrightarrow \exists z. (x = z^n \land \forall w. (z,w) \in R).$$
In the general case, we have a formula $$M = \{t(y_1,\dots,y_n,z_1,\dots,z_m) \mid \varphi(y_1,\dots,y_n,z_1,\dots,z_m)\},$$ where $t(y_1,\dots,y_n,z_1,\dots,z_m)$ is a term depending on $y_1,\dots,y_n,z_1,\dots,z_m$ and $\varphi(y_1,\dots,y_n,z_1,\dots,z_m)$ is a formula with free variables $y_1,\dots,y_n,z_1,\dots,z_m$ (and possibly further variables bound within $\varphi$). If the variables $y_1,\dots,y_n$ are bound outside of the set-builder notation, then $$x \in M \Leftrightarrow \exists z_1 \dots \exists z_m. (x = t(y_1,\dots,y_n,z_1,\dots,z_m) \land \varphi(y_1,\dots,y_n,z_1,\dots,z_m)).$$