I have been working on one of the problem like this:
$ x \in \wp(A \cap B) $
$ x \subseteq (A \cap B) $
$ \forall y (y \in x \implies y \in (A \cap B)) $
$ \forall y (y \in x \implies y \in A \land y \in B) $
$\forall y (y \notin x \lor (y \in A \land y \in B))$
$\forall y ((y \notin x \lor y \in A) \land (y \notin x \lor y \in B))$
$\forall y(y \in x \implies y \in A) \land \forall y(y \in x \implies y \in B)$
Now thinking over the last statement confuses me. Since y is a bound variable, I can replace it with any other variable:
$\forall y(y \in x \implies y \in A) \land \forall z(z \in x \implies z \in B)$
But doesn't replacing y with z in only one place fail to capture the fact they where reduced from the same y in the initial stages ?
It's possible to represent quantification without using variables at all. But we inherit a familiar and wonderfully flexible multi-part notation where we use e.g. $\forall \xi \ldots \xi \ldots \xi \ldots$ for the universal quantifier, meaning we insert a variable $\xi$ into some slot(s) in a predicate and prefix a matching quantifier $\forall \xi$ -- think of that as a single operation. As, for example, when we take the two-place predicate $\cdot R\cdot$, and quantify to get $\forall z\ zRz$.
But note, it is the whole multi-part expression that expresses the quantifier, and the choice of variable has zero significance. Its sole role is to link the quantifier to one or more particular slots in the predicate. When we have more than one quantifier around we need to use different variables to keep the linkages straight, but that's the only significance of the different variables.
It would be typographically messy but otherwise just as good simply to draw one or more arrow(s) with their tail(s) at the quantifier prefix and head(s) at the slot(s) in the predicate in order to indicate which quantifier is linked to which slot in a predicate.