According to Wikipedia
In the formal language of set theory, the axiom schema is: $$\forall w_1,\ldots ,w_n\forall A\exists B\forall x(x\in B\Leftrightarrow [x\in A\wedge \varphi(x,w_1,\ldots ,w_n,A)]).$$
It also emphasises that
... $B$ is not free in $\varphi$.
Questions: How to incorporate the above in the formalisation? And why does $A$ have to be free in $\varphi$?