Theorem cbvaliw

Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by NM, 19-Apr-2017.)

Hypotheses
cbvaliw.1
\( \vdash \forall x \, \varphi \rightarrow \forall y \, \forall x \, \varphi \)
cbvaliw.2
\( \vdash \neg \psi \rightarrow \forall x \, \neg \psi \)
cbvaliw.3
\( \vdash x = y \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \forall y \, \psi \)
Proof
l0
cbvaliw.1
l1
cbvaliw.2
\( \vdash \neg \psi \rightarrow \forall x \, \neg \psi \)
cbvaliw.3
\( \vdash x = y \rightarrow \varphi \rightarrow \psi \)
spimw l1 _
alrimih l0 _