First Quantifier Rule Questions

I need a little help with the proof of the validity of the first quantifier rule. So let $F \rightarrow G$ is valid in a structure $S$. I must prove that $\exists F(x) \rightarrow G$ is valid in $S$. Let $S$ be a $L$-structure. Suppose $F \rightarrow G$ is valid in $S$. For any term $t(x,y)$. So $t^S:S^{n+1} \rightarrow S$ and $(a,b) \rightarrow t^S(a,b) \in S$. So must show that $F^S(a,b)$ holds, then $G^S(a,b)$ holds. So i think I first should assume that $F^S(a,b)$ holds. Then should $(\exists F)^S(a,b)$ holds. I need to use the fact that $x$ is not free in $G$. Then use the lemma that says that if $x_i$ does not have a free occurrence in the formula $F(x_1,...,x_i,...,x_n)$ and $(a_1,...,a_i,...,a_n)\in F^S$ then, for any $a_i' \in S$, we have $(a_1,...,a_i',...,a_n)\in F^S$

Thanks for the help

We whave to show that :

if $F \rightarrow G$ is valid in $\mathcal S$ and $x \notin FV(G)$, then $\exists xF \rightarrow G$ is valid in $\mathcal S$.

Let $\mathcal S$ be a structure for the language $\mathcal L$. For each individual $a$ of $\mathcal S$, we choose a new constant, called the name of $a$. The first-order language obtained from $\mathcal L$ by adding all the names of individuals of $\mathcal S$ is designated by $\mathcal L(\mathcal S)$. We use $i$ as syntactical variable for names.

We say that, if $A$ is a formula of $\mathcal L$, an $\mathcal S$-instance of $A$ is a closed formula of the form $A[i_1, . . . , i_n]$ in $\mathcal L(\mathcal S)$.

We define the truth-value of a closed formula $A$ in $\mathcal L(\mathcal S)$ in the "usual" way, and we say that :

a formula $A$ of the language $\mathcal L$ is valid in $\mathcal S$ if $(A')^{\mathcal S} =$ TRUE for every $\mathcal S$-instance $A'$ of $A$.

Finally, we recall the semantical condition for $\exists$ :

we say that $(\exists x A)^{\mathcal S} =$ TRUE iff $(A_x[i])^{\mathcal S} =$ TRUE for some $i$ in $\mathcal L(\mathcal S)$.

Now for the proof, and assume for simplicity that $F$ has only $x$ as free variable.

Suppose that $F \rightarrow G$ is valid in $\mathcal S$, and that $x$ is not free in $G$, and suppose that $(\exists xF \rightarrow G)^{\mathcal S} =$ FALSE.

Then $(\exists xF)^{\mathcal S} =$ TRUE and $(G)^{\mathcal S} =$ FALSE.

From the former, $(F_x[i])^{\mathcal S} =$ TRUE for some $i$; so $(F_x[i] \rightarrow G)^{\mathcal S} =$ FALSE.

This is impossible, since $(F_x[i] \rightarrow G)^{\mathcal S}$ is an $\mathcal S$-instance of $F \rightarrow G$, which is valid in $\mathcal S$.

Thus, $(\exists xF \rightarrow G)^{\mathcal S} =$ TRUE.