question about set theory here, probably quite elementary.
When we use the notation $t\in\{x \mid \Phi(x) \}$, whether in an actual set theory or just as an abbreviation for $\Phi (t)$, must it be the case that the only free variable in $\Phi$ is $x$?
If not, what is the notation supposed to mean in the case that $\Phi$ has other free variables?
If $\Phi$ has other free variables... then $\{ x \mid \Phi \}$ is still the unique term with the property that $t \in \{ x \mid \Phi \}$ if and only if $\Phi[t/x]$. (assuming $x$ does not appear in the term $t$)