[proofplan]
Choose $\mathbb{P}$-names $\tau,\zeta \in M$ for $a$ and $z$. Inside $M$, use the definability of the forcing relation to build a name $\rho$ whose possible elements are exactly those names appearing in $\tau$ and whose tags force the desired formula. The verification has two inclusions: membership in $\rho_G$ implies membership in the separated subset by the [forcing theorem](/theorems/6531), and membership in the separated subset gives a forcing condition in the generic filter by the truth lemma and directedness of $G$.
[/proofplan]
[step:Choose names for the set and the parameter]
Since $a,z \in M[G]$, by the definition of the forcing extension there exist $\mathbb{P}$-names $\tau,\zeta \in M$ such that
\begin{align*}
\tau_G = a
\end{align*}
and
\begin{align*}
\zeta_G = z.
\end{align*}
We use the standard valuation of a name by a generic filter:
\begin{align*}
\theta_G = \{\sigma_G : \text{there exists } p \in G \text{ such that } (\sigma,p) \in \theta\}
\end{align*}
for every $\mathbb{P}$-name $\theta \in M$.
We also fix the forcing notation used below. For a condition $p \in \mathbb{P}$, a formula $\psi(v_1,\dots,v_n)$ of set theory, and $\mathbb{P}$-names $\theta_1,\dots,\theta_n \in M$, the expression
\begin{align*}
p \Vdash_{\mathbb{P}} \psi(\theta_1,\dots,\theta_n)
\end{align*}
means that $p$ forces the formula $\psi$ with the displayed names as parameters. Equivalently, for every $M$-generic filter $H \subseteq \mathbb{P}$ with $p \in H$, the forcing theorem gives
\begin{align*}
M[H] \models \psi((\theta_1)_H,\dots,(\theta_n)_H).
\end{align*}
The order convention is that $p \leq q$ means that $p$ is stronger than $q$; with this convention, a filter is upward closed from stronger conditions to weaker conditions.
[/step]
[step:Define the separating name inside $M$]
Let $S \in M$ be the set of first coordinates appearing in $\tau$:
\begin{align*}
S = \{\sigma : \text{there exists } q \in \mathbb{P} \text{ such that } (\sigma,q) \in \tau\}.
\end{align*}
This is a set in $M$ by Replacement applied in $M$ to the set $\tau$.
Define $B \in M$ by
\begin{align*}
B = \{p \in \mathbb{P} : \text{there exist } \sigma \in S \text{ and } q \in \mathbb{P} \text{ such that } (\sigma,q) \in \tau \text{ and } p \leq q\}.
\end{align*}
This is a subset of $\mathbb{P}$ definable in $M$ from $\tau$ and $\mathbb{P}$, so $B \in M$ by Separation in $M$.
Now define the $\mathbb{P}$-name $\rho$ by
\begin{align*}
\rho = \{(\sigma,p) \in S \times B : \text{there exists } q \in \mathbb{P} \text{ such that } (\sigma,q) \in \tau,\ p \leq q,\text{ and } p \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta)\}.
\end{align*}
The relation $p \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta)$ is definable over $M$ by the forcing theorem (citing a result not yet in the wiki: Forcing Theorem). Therefore $\rho$ is a subset of the set $S \times B$ definable in $M$ from parameters $\tau,\zeta,\mathbb{P}$, and Separation in $M$ gives $\rho \in M$.
[guided]
The goal is to build, before passing to the extension, a name whose interpretation will be the separated subset. Since $a=\tau_G$, every possible element of $a$ has the form $\sigma_G$ for some first coordinate $\sigma$ appearing in $\tau$. We therefore define
\begin{align*}
S = \{\sigma : \text{there exists } q \in \mathbb{P} \text{ such that } (\sigma,q) \in \tau\}.
\end{align*}
Because $\tau$ is a set in $M$, the collection of its first coordinates is also a set in $M$.
Next we restrict the possible tags. If a condition $p$ is to certify that $\sigma_G$ belongs to the separated subset, then $p$ should strengthen some condition $q$ already tagging $\sigma$ in $\tau$. This motivates
\begin{align*}
B = \{p \in \mathbb{P} : \text{there exist } \sigma \in S \text{ and } q \in \mathbb{P} \text{ such that } (\sigma,q) \in \tau \text{ and } p \leq q\}.
\end{align*}
This is a subset of the forcing poset $\mathbb{P}$, and the defining condition only uses parameters belonging to $M$. Since $M \models \mathrm{ZFC}$, Separation inside $M$ gives $B \in M$.
We now define
\begin{align*}
\rho = \{(\sigma,p) \in S \times B : \text{there exists } q \in \mathbb{P} \text{ such that } (\sigma,q) \in \tau,\ p \leq q,\text{ and } p \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta)\}.
\end{align*}
The important point is that this is not a proper class construction. The pair $(\sigma,p)$ ranges over the set $S \times B$, and the additional predicate $p \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta)$ is definable over $M$ by the forcing theorem (citing a result not yet in the wiki: Forcing Theorem). Thus the defining condition is a legitimate formula over $M$ with parameters in $M$. Applying Separation in $M$ to the set $S \times B$ gives $\rho \in M$.
[/guided]
[/step]
[step:Show that every element of $\rho_G$ satisfies the separating formula]
Let $x \in \rho_G$. By the valuation definition, there exist a name $\sigma \in M$ and a condition $p \in G$ such that
\begin{align*}
(\sigma,p) \in \rho
\end{align*}
and
\begin{align*}
x = \sigma_G.
\end{align*}
By the definition of $\rho$, there exists $q \in \mathbb{P}$ such that
\begin{align*}
(\sigma,q) \in \tau,
\end{align*}
\begin{align*}
p \leq q,
\end{align*}
and
\begin{align*}
p \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta).
\end{align*}
Since $G$ is a filter and $p \in G$ with $p \leq q$, the upward closure convention for filters gives $q \in G$. Hence $\sigma_G \in \tau_G$, so
\begin{align*}
x \in a.
\end{align*}
Also, since $p \in G$ and $p \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta)$, the forcing theorem gives
\begin{align*}
M[G] \models \varphi(\sigma_G,\zeta_G).
\end{align*}
Using $\sigma_G=x$ and $\zeta_G=z$, we obtain
\begin{align*}
M[G] \models \varphi(x,z).
\end{align*}
Therefore
\begin{align*}
\rho_G \subseteq \{x \in a : M[G] \models \varphi(x,z)\}.
\end{align*}
[/step]
[step:Show that every element satisfying the formula is named by $\rho$]
Let
\begin{align*}
x \in \{y \in a : M[G] \models \varphi(y,z)\}.
\end{align*}
Then $x \in a=\tau_G$, so by the valuation definition there exist a name $\sigma \in M$ and a condition $q \in G$ such that
\begin{align*}
(\sigma,q) \in \tau
\end{align*}
and
\begin{align*}
\sigma_G = x.
\end{align*}
Since $M[G]\models \varphi(x,z)$, and since $x=\sigma_G$ and $z=\zeta_G$, we have
\begin{align*}
M[G]\models \varphi(\sigma_G,\zeta_G).
\end{align*}
By the [truth lemma for forcing](/theorems/6518) (citing a result not yet in the wiki: Truth Lemma), there exists $p_0 \in G$ such that
\begin{align*}
p_0 \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta).
\end{align*}
Because $G$ is a filter, it is directed downward with respect to the order $\leq$. Hence, from $p_0,q \in G$, there exists $r \in G$ such that
\begin{align*}
r \leq p_0
\end{align*}
and
\begin{align*}
r \leq q.
\end{align*}
Forcing is monotone under strengthening, so from $r \leq p_0$ and $p_0 \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta)$ we get
\begin{align*}
r \Vdash_{\mathbb{P}} \varphi(\sigma,\zeta).
\end{align*}
Together with $(\sigma,q)\in\tau$ and $r \leq q$, the definition of $\rho$ gives
\begin{align*}
(\sigma,r) \in \rho.
\end{align*}
Since $r \in G$, the valuation definition yields $\sigma_G \in \rho_G$. Thus $x=\sigma_G \in \rho_G$, proving
\begin{align*}
\{x \in a : M[G] \models \varphi(x,z)\} \subseteq \rho_G.
\end{align*}
[/step]
[step:Identify the separated subset as an element of the extension]
Combining the two inclusions, we have
\begin{align*}
\rho_G = \{x \in a : M[G] \models \varphi(x,z)\}.
\end{align*}
Since $\rho \in M$ is a $\mathbb{P}$-name, its valuation $\rho_G$ belongs to $M[G]$ by the definition of the forcing extension. Therefore
\begin{align*}
\{x \in a : M[G] \models \varphi(x,z)\} \in M[G].
\end{align*}
This proves Separation in the forcing extension.
[/step]
