Prove $\forall z\left(\left(\exists xA\rightarrow A_{x}[z]\right)\rightarrow B\right)\vDash B$ I'm doing some self-exercises on mathematical logic by myself and have come across this question which I can't seem to prove:

Let $A$ be a formula with a single free variable $x$. Let $B$ be a
  formula also, and $z$ be a variable that does not appear in $A$ or in
  $B$
Prove:
$\forall z\left(\left(\exists xA\rightarrow A_{x}[z]\right)\rightarrow B\right)\vDash B$

My train of thought was this:
The meaning of $A \vDash B$ is that a structure that satisfies A also satisfies B: $M \vDash A \Rightarrow M \vDash B$ 
With that in mind, I started trying to understand what the meaning of $ C = (\exists xA\rightarrow A_{x}[z])$ was, and came to the conclusion that if said formula C is always $True$ then I would get the following:
$(True) \rightarrow B = \urcorner(True) \vee B = (False) \vee B $ 
And in this situation, for a structure to satisfy C it has to satisfy B thus proving the claim.
The thing is that I don't know (or know how to prove) if C is always $True$. It seems logical in a way, since if I am replacing all free occurrences of $x$ by $z$ (which does not appear in A) then A itself doesn't really change and so C will be $True$ depending if the structure satisfies A or not.
Is my train of thought OK? or am I missing something?
Is there maybe another way of proving it? 
Thank you to anyone who helps!
 A: I suggest to work with Rob's comment above.
We have that :

$\vDash (∃xβ → α) ↔ ∀x(β → α)$, if $x$ does not occur free in $\alpha$.

Thus : $\forall z [(\exists x A(x) \rightarrow A(x/z)) \rightarrow B]$ is equivalent to : $\exists z (A(x) \rightarrow A(x/z)) \rightarrow B$.
We have also that :

$\vDash (α → ∃xβ) ↔ ∃x(α → β)$, if $x$ does not occur free in $\alpha$.

Thus : $\exists z (A(x) \rightarrow A(x/z))$ is equivalent to : $A(x) \rightarrow \exists z A(z)$.
In conclusion, our formula is equivalent to :

$(A(x) \rightarrow \exists z A(z)) \rightarrow B$

and the antecedent is valid.
We can now use the heuristic considerations above to prove it "semantically".
Consider a structure $\mathcal M$ such that $\mathcal M \vDash \forall z [(\exists x A(x) \rightarrow A(x/z)) \rightarrow B]$.
We have two cases : if $\mathcal M \vDash B$ we are done.
Assume insted that we have : $\mathcal M \nvDash B$; but then we must have that $(\exists x A(x) \rightarrow A(x/z))[d]$ must be falsified for all $d \in |\mathcal M|$, and this is impossible.

We can prove with Natural Deduction that :


$\forall z [(∃xA(x) \rightarrow A(z)) \rightarrow B] \vdash B$.


Proof :

1) $\forall z [(∃xA(x) \rightarrow A(z)) \rightarrow B]$ --- premise

2) $(∃xA(x) \rightarrow A(z)) \rightarrow B$ --- from 1) by $\forall$-elimination 
3) $\lnot A(z)$ --- assumed [a]
4) $\forall x \lnot A(x)$ --- from 3) by $\forall$-introduction
5) $\lnot \exists x A(x)$ --- from 4) with : $\forall x \lnot A(x) \rightarrow \lnot \exists x A(x)$ by $\rightarrow$-elimination
6) $\exists x A(x)$ --- assumed [b] 
7) $\bot$ --- from 5) and 6) by $\rightarrow$-elimination
8) $A(z)$ --- from 3) and 7) by Double Negation, discharging [a]
9) $\exists x A(x) \rightarrow A(z)$ --- from 6) and 8) by $\rightarrow$-introduction, discharging [b]

10) $B$ --- from 2) and 9) by $\rightarrow$-elimination.

