In "Handbook of Model Checking" (p. 37, 2.2.4 Algorithms), the following operator is presented (along with 3 similar ones):
$$\mathrm{prime}(\tau)=\exists\mathscr{V}.(\tau\land({\bigwedge}_{v\in\mathscr{V}}v=v'))$$
From the text, it seems that this is supposed to replace each instance of a variable $v\in\mathscr{V}$ that occurs in the assertion $\tau$ with its primed counterpart $v'\in\mathscr{V'}$.
For example, $\mathrm{prime}(x=3)$ should be equivalent to $x'=3$.
Note that $\mathscr{V}$ and $\mathscr{V'}$ are fixed in this context to be sets which contain all of the variables in the domain of discourse and their primed counterparts, respectively ($\mathscr{V}=\{x\}$ and $\mathscr{V'}=\{x'\}$ in the above example).
I'm having trouble understanding how exactly the existential quantifier works in this context.
To follow the above example, with $\tau$ defined as $x=3$ and $\mathscr{V}$ defined as $\{x\}$, we have (by simple variable replacement):
$$\mathrm{prime}(x=3)=\exists\{x\}.((x=3)\land(x=x'))$$
Or, equivalently:
$$\mathrm{prime}(x=3)=\exists\{x\}.(x=x'=3)$$
This is where I'm stuck. The text says that the existential quantifier "quantifies out" variables in $\mathscr{V}$. I expect from context that this allows us to "remove" the $x$ instance on the right hand side (as I expect the result to simplify to $x'=3$), but I don't understand how/why this is possible. What am I missing? Perhaps this example is too simple? This pattern appears in several other works in this space (model checking) and while I can accept simple operators like $\mathrm{prime}$ at face value, some of the more complex ones are harder to understand, and I feel this is holding me back.
Thanks in advance!