My question concerns the proof of Theorem II.4.2 below in Logical Foundations of Proof Complexity by Cook and Nguyen, which relies on Corollary II.3.5 below. Corollary II.3.5 is the derivational soundness of completeness of LK when the first order language $\mathcal{L}$ contains the equality symbol. The book initially presents this result in a previous section when $\mathcal{L}$ does not contain the equality symbol, and addresses the case when $\mathcal{L}$ does contain equality in Corollary II.3.5 by introducing the following set of "equality axioms".
Definition Let $\mathcal{L}$ be a first order vocabulary. Then define $\mathcal{E}_\mathcal{L}$ as the following set of $\mathcal{L}$ sentences.
EA1: $\forall x (x = x)$
EA2: $\forall x \forall y (x = y \supset y = x)$
EA3: $\forall x \forall y \forall z (x = y \land y = z \supset x = z)$
EA4: For any $m$-ary function symbol $f \in \mathcal{L}$,
$$\forall x_1 ... \forall x_m \forall y_1 ... \forall y_m (x_1 = y_1 \land ... \land x_m = y_m \supset f(x_1,...,x_m) = f(y_1,...,y_m))$$
EA5: For any $m$-ary predicate symbol $P \in \mathcal{L}$,
$$\forall x_1 ... \forall x_m \forall y_1 ... \forall y_m (x_1 = y_1 \land ... \land x_m = y_m \supset (P(x_1,...,x_m) \supset P(y_1,...,y_m)))$$
If $B$ is a formula, we define the universal closure $\forall B$ of $B$ as the sentence $\forall b_1 ... \forall b_k B$, where $b_1,...,b_k$ is the set of all free variables occurring in $B$. For a set $\Phi$ of formulas, we define the universal closure $\forall \Phi$ of $\Phi$ as the set of sentences $\forall B$ for each $B \in \Phi$.
Corollary II.3.5: Let $\mathcal{L}$ be a first-order vocabulary, $\Phi$ be a set of $\mathcal{L}$ formulas and $A$ be a $\mathcal{L}$ formula. Then $\forall \Phi \vDash A$ iff there is an LK-$\Psi$ proof of $A$, where $\Psi = \Phi \cup \mathcal{E}_\mathcal{L}$.
Theorem II.4.2 (Compactness): If $\Phi$ is an unsatisfiable set of formulas, then a finite subset of $\Phi$ is unsatisfiable.
Proof: First note that we may assume that $\Phi$ is a set of sentences, by replacing the free variables in $\Phi$ by distinct new constant symbols. The resulting set of sentences is satisfiable iff the original set of formulas is satisfiable. Since $\Phi$ is unsatisfiable iff the empty sequent $\rightarrow$ is a logical consequence of $\Phi$, and since LK-$\Psi$ proofs are finite, the theorem now follows from Corollary II.3.5.
My Question
Why do we need to assume that $\Phi$ is a set of sentences in the proof of Theorem II.4.2? Corollary II.3.5 works when $\Phi$ is an arbitrary set of formulas (not necessarily sentences). I recognize that we need to state derivational soundness of LK we require $\forall \Phi \vDash A$ as our assumption, since not all of the rules of LK are sound unless the formulas involved are universally closed. However, the same requirement does not hold for derivational completeness of LK, which is the direction of Corollary II.3.5 we rely on in the proof of Theorem II.4.2. To be more precirse, couldn't we use the following proposition instead?
Proposition: If $\Phi \vDash A$, then there is an LK-$\Psi$ proof of $A$ where $\Psi := \Phi \cup \mathcal{E}_\mathcal{L}$.
The proof follows immediately from the fact that $\Phi \vDash A$ implies $\forall \Phi \vDash A$ and the completeness direction of Corollary II.3.5.