Is $\forall x (\phi)$ a formula in ZF even if $\phi$ does not contain x? I was reading A Quick Introduction To Basic Set Theory by Anush Tserunyan, and in definition 1.1, the author defined a notation of a formula in ZF with few criterias. One of them states:

If $\phi$ is a formula and $x$ is a variable, then $\forall x(\phi)$ and $\exists x(\phi)$ are formulas.

I remember in first-order logic, the formula is defined similarly, but it requires $\phi$ to contain the restricting variable, namely, x, in the above. Is it different in the case of ZF and can we write something like $\forall x(y=y)$?
Also, the author also said that $\phi(x)$ emphasized that this formula "says something about a set (variable) x". Should I assume this implies $\phi(x)$ must contains x? (for instance, in the case of axiom schema 5 of Comprehension.)
 A: You're mistaken about first-order logic - there is no such requirement. $\forall x\,(y=y)$ is a perfectly good formula of first-order logic (and of ZF set theory).
When we write $\varphi(x_1,\dots,x_n)$, we mean that the only variables occurring free in $\varphi$ are among the $n$ variables $x_1,\dots,x_n$. There is no requirement that all $n$ of these variables actually appear free in $\varphi$. For example, $\varphi(x)$ might be $\exists y\,(y=y)$. We can interpret this formula as saying something about $x$, just not something interesing!
A: I'll go over how formula are constructed in ZFC.
Atomic Formula are formula of the form:
$x_i$∈$x_j$; $x_i$=$x_j$
where i,j are natural numbers.
If $\phi$ and $\varphi$ are Formula, then
$\phi$ ∧ $\varphi$
$\neg \phi$
(∃$x_i)\phi$
are all formula.
These are sufficient, since we can build disjunction,universal quantification, and implication by just applying these.
Notice that:
If $\phi$ is the formula $x_2$=$x_2$
then:
(∃$x_4)(x_2=x_2$)
is a formula.
Definition: Let ψ be a quantifier
then (ψ$x_j$)$\phi$ is a formula, we say that   (ψ$x_j$)$\phi$ is in the scope of (ψ$x_j$)
An instance of a variable is bound if lies in the scope of a quantifier acting on that same variable. i.e. if the variable that the quantifier is acting on occurs in the scope, it is an instance of a bound variable.
An instance of a variable is free if it is not bounded.
So, In (∃$x_4)(x_2=x_2$)
$x_4$ is bounded, and $x_2$ is free
Notice that the formula doesn't say anything about $x_4$. If instead it was $x_5$ the formula would be the same.
Formula say things about their free variables. They express properties about their free variables.
So, here we would say $\phi(x_2)$ to emphasize that $x_2$ is a free variable i.e. it is not bounded. However, $x_2$ need not appear anywhere in the formula, and there may be other variables which are free, that are just not being given emphasis.
Bounded variables are merely "dummy variables", whether it's $x_4$ or $x_5$ doesn't actually change anything in terms of the truth value of $\phi$
Another Example:
$x_2$ = $x_4$ ∧ (∃$x_4)(x_2∈x_4)$
All instances of $x_2$ are free, so $x_2$ is free.
The first instance of $x_4$ is free,
but the second instance of $x_4$ is bounded, as is the third instance.
As bounded variables are "dummy". Their choice is arbitrary.
So,
(∃$x_2)\phi(x_1)$
(∃$x_3)\phi(x_1)$
are equivalent
