Theorem cbvaldvaw

Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. Version of cbvaldva with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid [ax-13]. (Revised by GG, 10-Jan-2024.) Reduce axiom usage, along an idea of GG. (Revised by Wolf Lammen, 10-Feb-2024.)

Hypothesis
cbvaldvaw.1
\( \vdash \varphi \wedge x = y \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\forall x \, \psi \leftrightarrow \forall y \, \chi) \)
Proof
cbvaldvaw.1
ancoms _
pm5.74da _
l3
cbvalvw _
\( \vdash \forall x \, (\varphi \rightarrow \psi) \leftrightarrow \forall y \, (\varphi \rightarrow \chi) \)
l4
19.21v
\( \vdash \forall x \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow \forall x \, \psi \)
19.21v
\( \vdash \forall y \, (\varphi \rightarrow \chi) \leftrightarrow \varphi \rightarrow \forall y \, \chi \)
3bitr3i l3 l4 _
pm5.74ri _