Theorem cbv2w
Rule used to change bound variables, using implicit substitution.
Version of cbv2 with a disjoint variable condition, which does not
require [ax-13]. (Contributed by NM, 5-Aug-1993.) Avoid [ax-13].
(Revised by GG, 10-Jan-2024.)
Hypotheses
cbv2w.1
\( \vdash \Finv x \, \varphi \)
cbv2w.2
\( \vdash \Finv y \, \varphi \)
cbv2w.3
\( \vdash \varphi \rightarrow \Finv y \, \psi \)
cbv2w.4
\( \vdash \varphi \rightarrow \Finv x \, \chi \)
cbv2w.5
\( \vdash \varphi \rightarrow x = y \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\forall x \, \psi \leftrightarrow \forall y \, \chi) \)
Proof
l0
cbv2w.1
l1
cbv2w.2
l2
cbv2w.3
l3
cbv2w.4
l4
cbv2w.5
\( \vdash \varphi \rightarrow x = y \rightarrow (\psi \leftrightarrow \chi) \)
biimp
\( \vdash (\psi \leftrightarrow \chi) \rightarrow \psi \rightarrow \chi \)
syl6 l4 _
l7
cbv1v l0 l1 l2 l3 _
l8
cbv2w.2
l9
cbv2w.1
l10
cbv2w.4
l11
cbv2w.3
l12
equcomi
\( \vdash y = x \rightarrow x = y \)
l13
cbv2w.5
\( \vdash \varphi \rightarrow x = y \rightarrow (\psi \leftrightarrow \chi) \)
biimpr
\( \vdash (\psi \leftrightarrow \chi) \rightarrow \chi \rightarrow \psi \)
syl56 l12 l13 _
cbv1v l8 l9 l10 l11 _
impbid l7 _