Converting open first order logic formulae to closed formulae Let $A \in WFF_{FOL}^\Sigma$ be an open formula, ie. it has occurrences of free variables. How do you transform this formula into a closed formula $B$?
It is my impression that you do this by adding, for each free variable in $A$, a universal quantifier to capture that variable. e.g., if $A = \exists x R(x,y,z)$, then $B = \forall y \forall z (\exists x R(x,y,z))$, and $A ↔ B$. Another example; $A = \exists x R(x,y) → \forall x P(x,z)$, $B = \forall y \forall z (\exists x R(x,y) → \forall x P(x,z))$Since all the quantifiers that you add to $A$ are universal, I also think that the order that you add these quantifiers in does not matter. 
Logical Equivalence?
It turns out that, with the definitions that I am working with, translating an open formula to a closed formula yields a closed formula that is satisfiable in the same structure as the open formula. Logical equivalence is a special case of this. If you are working with other definitions, it may be that you get logically equivalent formulae by translating from open to closed formula. 

Definitions ($A$ and $B$  are formulae, $M$ is a structure, $v$ is an assignment)
$A$ is valid iff for all structures  $M : M ⊨ A$
$B \Rightarrow A$: $\forall v. M \models_v B → A$
$B \models A$: $\forall M. \, \text{if} \, (\forall v. M \models_v B) \, \text{then}\, (\forall u . M \models_u A)$
If $A$ and $B$ are closed formulae: $B \models A$ iff $B \Rightarrow A$. (This does not hold, in general, for open formulae.)
$A \Leftrightarrow B$ iff $A \Rightarrow B$ and $B \Rightarrow A$ (logical equivalence)

In Metamath, both $φ ⊢ ∀ \: x \: φ$ and $∀ \: x \: φ ⊢ φ$ are provable whether $x$ occurs in $φ$ or not (1, 2). $φ → ∀ \: x \: φ$ and $∀ \: x \: φ → φ$ are also provable, but the first only if $x$ does not occur in $φ$ (3, 4). Allegranza's answer instanciates $φ$ both with $0 = 0$ and $x = 0$.
