The proof is OK. Here are some small details.
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
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, ."