Theorem cbvalw

Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.)

Hypotheses
cbvalw.1
\( \vdash \forall x \, \varphi \rightarrow \forall y \, \forall x \, \varphi \)
cbvalw.2
\( \vdash \neg \psi \rightarrow \forall x \, \neg \psi \)
cbvalw.3
\( \vdash \forall y \, \psi \rightarrow \forall x \, \forall y \, \psi \)
cbvalw.4
\( \vdash \neg \varphi \rightarrow \forall y \, \neg \varphi \)
cbvalw.5
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \forall x \, \varphi \leftrightarrow \forall y \, \psi \)
Proof
l0
cbvalw.1
l1
cbvalw.2
cbvalw.5
biimpd _
l4
cbvaliw l0 l1 _
l5
cbvalw.3
l6
cbvalw.4
cbvalw.5
biimprd _
equcoms _
cbvaliw l5 l6 _
impbii l4 _