Theorem cbvsbv

Change the bound variable (i.e. the substituted one) in wff's linked by implicit substitution. The proof was extracted from a former [cbvabv] version. (Contributed by Wolf Lammen, 16-Mar-2025.)

Hypothesis
cbvsbv.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash [ z' / x ] \, \varphi \leftrightarrow [ z' / y ] \, \psi \)
Proof
l0
sbco2vv
\( \vdash [ z' / y ] \, [ y / x ] \, \varphi \leftrightarrow [ z' / x ] \, \varphi \)
cbvsbv.1
sbievw _
sbbii _
\( \vdash [ z' / y ] \, [ y / x ] \, \varphi \leftrightarrow [ z' / y ] \, \psi \)
bitr3i l0 _