Theorem cbvsbvf
Change the bound variable (i.e. the substituted one) in wff's linked by
implicit substitution. The proof was part of a former [cbvabw] version.
(Contributed by GG and WL, 26-Oct-2024.)
Hypotheses
cbvsbvf.1
\( \vdash \Finv y \, \varphi \)
cbvsbvf.2
\( \vdash \Finv x \, \psi \)
cbvsbvf.3
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash [ z' / x ] \, \varphi \leftrightarrow [ z' / y ] \, \psi \)
Proof
l0
nfv
cbvsbvf.1
l2
nfim l0 _
l3
nfv
cbvsbvf.2
l5
nfim l3 _
l6
equequ1
cbvsbvf.3
imbi12d l6 _
cbvalv1 l2 l5 _
imbi2i _
l11
albii _
\( \vdash \forall w \, (w = z' \rightarrow \forall x \, (x = w \rightarrow \varphi)) \leftrightarrow \forall w \, (w = z' \rightarrow \forall y \, (y = w \rightarrow \psi)) \)
l12
dfsb
\( \vdash [ z' / x ] \, \varphi \leftrightarrow \forall w \, (w = z' \rightarrow \forall x \, (x = w \rightarrow \varphi)) \)
dfsb
\( \vdash [ z' / y ] \, \psi \leftrightarrow \forall w \, (w = z' \rightarrow \forall y \, (y = w \rightarrow \psi)) \)
3bitr4i l11 l12 _