Let $P$ be a poset and $\sigma$ be a $P$-name. We call $\tau \in V^P$ a nice name for a subset of $\sigma$ when $\tau$ is of the form $\bigcup \{\{\pi\} \times A_\pi : \pi\in\operatorname{dom}\sigma\}$, where $A_\pi\subseteq P$ is an antichain in $V$.
It is known that for each $\sigma,\,\mu\in V^P$ we can find a nice name $\tau$ for a subset of $\sigma$ such that $$1\Vdash \mu\subseteq \sigma \to \tau=\mu.$$ (e.g. Chapter VII, 5.12 of Kunen's book published in 1980.)
A proof of the theorem I have known uses semantic characterization of the forcing. I wonder there is a synthetic proof of the theorem, that is, a proof which does not rely on a generic filter.
Of course, we don't need to consider nice names if we use Boolean-valued models. I am wondering a proof which does not use Boolean-valued models too. Thanks for any help!
I have tried proving my question again after reading Asaf's comment, and get a proof of it. Here is my proof:
Assume that $p_0 \Vdash \mu\subseteq \sigma$. We shall prove that $p_0$ forces both $\tau\subseteq \mu$ and $\mu\subseteq \tau$. Here $\tau$ is the nice name whose definition is given by Asaf.
First, we will prove $p_0\Vdash \tau\subseteq \mu$. Let $(\pi,s_\pi)\in\tau$. By definition of $\tau$, $s_\pi\Vdash \pi\in \mu$. We have to prove for each $p\le p_0$ there is $q\le p$ such that $$q\le s_\pi\implies \exists (\rho,s_\rho)\in\mu : q\le s_\rho \text{ and } q\Vdash \pi=\rho.$$
If $p\perp s_\pi$, then no $q\le p$ would satisfy $q\le s_\pi$, so we are done. Otherwise, fix $p_1$ a common extension of $p$ and $s_\pi$. Then we have $p_1\Vdash \pi\in\mu$. Therefore, by the synthetic characterization of $p\Vdash \pi\in\mu$ we can find desired $q\le p_1$ and $(\rho,s_\rho)\in\mu$.
To finish the proof we will prove $p_0\Vdash \mu\subseteq\tau$. For each $(\pi,s_\pi)\in\mu$ we have $p_0\Vdash \mu\subseteq \sigma$. Hence the following holds: $$\forall p\le p_0\exists q_0\le p : q_0\le s_\pi \implies \exists (\rho,s_\rho)\in\sigma : q_0\le s_\rho\text{ and } q_0\Vdash \pi=\rho.\qquad \cdots\cdots\,(*)$$
We will prove that for each $p$ we can find $\rho\in V^P$ and $q\le p$ such that $$q\le s_\pi \implies \exists \tilde{s}_\rho : (\rho,\tilde{s}_\rho)\in\tau,\, q\le \tilde{s}_\rho\text { and } q\Vdash \pi=\rho.$$
If $q_0$ is not an extension of $s_\pi$, take $q=q_0$. If not, there is $(\rho,s_\rho)\in\sigma$ satisfying $(*)$. Notice that $q_0\Vdash \pi=\rho$ implies $q_0\Vdash \pi\in\mu$, hence there is $q_1\in A_\pi$ such that $q_0$ and $q_1$ have a common extension $q$. Here $q$ satisfies
Therefore we have found a desired $q$.