I am currently studying axiomatic set theory and I am struggle to answer some questions regarding the axiom schema of separation. First, let me introduce some context. It is usual to state the axiom schema of separation as
$$\vdash \forall y \exists x \forall z (z \in x) \leftrightarrow (z \in y \wedge \phi(z))$$
regarded that $z$ is a free variable in $\phi$ and that $x$ is not a free variable in $\phi$.
In the presence of the logical axioms concerning universal quantification, one can deduce a more general version of this axioms, for example
$$\vdash \forall w_1 \forall w_2 \cdots \forall w_n \forall y \exists x \forall z (z \in x) \leftrightarrow (z \in y \wedge \phi(z,w_1,w_2, \dots, w_n)).$$
One may even allow the variable $y$ to occur in the formula $\phi$ as a free variable and we obtain something similar to the previous one, which $\phi(z,y,w_1,\dots,w_n)$ in the place of $\phi(z,w_1,w_2,\dots,w_n)$.
Now, just a couple of things concerning the presented until now. When I ask if something is correct or true, I am actually asking if the reasons that I am giving are the ones that motivates the formulation of this axiom schema.
I believe that the reason that we do not allow $x$ to be a free variable in the formula $\phi$ is because otherwise we would be defining the set $x$ in terms of the set $x$ (informally, it happens self referencing). Is this correct? Also, I think that we do not state anything about the possibility of $x$ being a bound variable in $\phi$ since we cal always change the bound occurrences of a variable for another variable which do not appear in the formula. Is it true?
Regarding the variable $z$. We do not worry abound the bound occurrences since, as it was said in the last paragraph, we can always change them for some other variable which do not occur in the formula. The fact that $z$ must occur free in $\phi$ sounds intuitively plausible, since we are “testing” the elements that came from why to see if they satisfy the formula $\phi$ so we can gather them together. Right?
About allowing $y$ to be also a free variable in $\phi$. Well I must say that his one I can’t figure it out. I mean, we can check a few examples and intuitively they seem sound, but I wonder why would someone use this an instance of this axiom schema, while letting the variable $y$ to be free in $\phi$.
This are my main questions. I must say that (obviously) I am not trying to prove the axiom schema, I am just trying to get a feel for it and to come up with an informal justification of how it was formulated.
Also, when dealing axiomatically, one observes that the variables play the roles of sets in the language of set theory, meaning, a variable is used to denote sets. But is it right to say, for example, “$x$ is a set which do not occur free in $\phi$“? In other words, variables and sets are different things (I guess?)
Thank you in advance!