Theorem cbvaldw

Deduction used to change bound variables, using implicit substitution. Version of cbvald with a disjoint variable condition, which does not require [ax-13]. (Contributed by NM, 2-Jan-2002.) Avoid [ax-13]. (Revised by GG, 10-Jan-2024.)

Hypotheses
cbvaldw.1
\( \vdash \Finv y \, \varphi \)
cbvaldw.2
\( \vdash \varphi \rightarrow \Finv y \, \psi \)
cbvaldw.3
\( \vdash \varphi \rightarrow x = y \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\forall x \, \psi \leftrightarrow \forall y \, \chi) \)
Proof
l0
nfv
l1
cbvaldw.1
l2
cbvaldw.2
l3
nfvd
cbvaldw.3
cbv2w l0 l1 l2 l3 _