Suppose I have a set defined as:
$$A = \{x \in X : \phi(x)\}$$
Then, the statement $a \in A$ can be symbolised in FOL as:
$$\forall x(x \in A \leftrightarrow (x \in X \land \phi(x)))$$
For example:
Define a relation $R \subseteq A\times B$. Then, $b \in Dom(R^{-1})$ would be symbolised as:
$$b \in \{y \in B : \exists x(x \in A \land (y,x) \in R^{-1}\}$$ $$b \in B \land \exists x(x \in A \land (b,x) \in R^{-1})$$
On
$\{x\in X: \phi(x)\}$ is the "set of elements of $X$ where $\phi(x)$ holds", or "the subset of $X$ whose elements satisfy $\phi$". The colon punctuation separates the generic element from its construction, and is technically not a conjunction. It is read as "where" or "such that", since this is the set of $x$ that are things, not the set of $x$ and other things. However, we may write the set as $\{x: x\in X\wedge \phi(x)\}$, the "set of $x$ that are in $A$ and satisfy $\phi(x)$".
So, the statement $A=\{x\in X:\phi(x)\}$ is equivalent to $\forall x~.(x\in A\leftrightarrow x\in X\wedge \phi(x))$.
If $R\subseteq A\times B$ , then the domain of the inverse of $R$ is the set of elements in $B$ that $R^{-1}$ maps to some element in $A$, which is to say: $$\operatorname{Dom}(R^{-1}) = \{y\in B: \exists x~. (x\in A\land\langle y,x\rangle\in R^{-1})\}$$
That says $\forall b~.(b\in\operatorname{Dom}(R^{-1}) \leftrightarrow \exists a~.(a\in A\wedge \langle b,a\rangle\in R^{-1}))$.
Yes, your formalization is correct, except that if you define $$\tag{1} A = \{x \in X : \phi(x)\}$$ then $(1)$ can be formalized by formula $(4)$ below. As a consequence, $$\tag{2}a \in A$$ means $$\tag{3} a \in X \land \phi(a)$$ and not $$\tag{4} \forall x (x \in A \leftrightarrow (x \in X \land \phi(x)))$$ since $a$ does not occur in $(4)$. In other words, saying $(1)$ is equivalent to say $(4)$, and as a consequence, $(2)$ is equivalent to $(3)$.
Formalization $(3)$ is what you actually used to "translate" the meaning of $b \in \mathrm{Dom}(R^{-1})$ in your example.
As you correctly pointed out, colon "$:$" in $(1)$ is translated by a conjunction $\land$ in formalization $(4)$.
By the way, note that formalizations $(3)$ and $(4)$ are not "completely logical" in the sense that the meaning of the symbol $\in$ is not logical, but it is given by the axioms of set theory.