I think it should say "satisfy" because A and s together satisfy .

The proof is OK. Here are some small details.

Do you mean they are equal as predicates on structures? If so, it's fine; otherwise, it is safer to say " iff for any structure B," or " iff ." This equivalence (or equality) is the key lemma in the proof, which has to be proved before, probably by induction on formulas using the precise definition of free occurrence.

Also, it would be better to make the scope of d more explicit. This means writing "for all d" and making sure that when you conclude , no open assumption contains d. So, instead of

I would write,

Since x does not occur free in , for all d we have that iff , and so .

Then the scope of d is the sentence above, which proves "for all d, ."