Theorem cbvaldva

Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker cbvaldvaw if possible. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.)

Hypothesis
cbvaldva.1
\( \vdash \varphi \wedge x = y \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\forall x \, \psi \leftrightarrow \forall y \, \chi) \)
Proof
l0
nfv
l1
nfvd
cbvaldva.1
ex _
cbvald l0 l1 _