Theorem cbvalvw

Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Feb-2018.)

Hypothesis
cbvalvw.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \forall x \, \varphi \leftrightarrow \forall y \, \psi \)
Proof
l0
ax-5
l1
ax-5
l2
ax-5
l3
ax-5
cbvalvw.1
cbvalw l0 l1 l2 l3 _