Theorem cbv2
Rule used to change bound variables, using implicit substitution. Usage
of this theorem is discouraged because it depends on [ax-13]. See
cbv2w with disjoint variable conditions, not depending on [ax-13].
(Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro,
3-Oct-2016.) Format hypotheses to common style, avoid [ax-10].
(Revised by Wolf Lammen, 10-Sep-2023.) (New usage is discouraged.)
Hypotheses
cbv2.1
\( \vdash \Finv x \, \varphi \)
cbv2.2
\( \vdash \Finv y \, \varphi \)
cbv2.3
\( \vdash \varphi \rightarrow \Finv y \, \psi \)
cbv2.4
\( \vdash \varphi \rightarrow \Finv x \, \chi \)
cbv2.5
\( \vdash \varphi \rightarrow x = y \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\forall x \, \psi \leftrightarrow \forall y \, \chi) \)
Proof
l0
cbv2.1
l1
cbv2.2
l2
cbv2.3
l3
cbv2.4
l4
cbv2.5
\( \vdash \varphi \rightarrow x = y \rightarrow (\psi \leftrightarrow \chi) \)
biimp
\( \vdash (\psi \leftrightarrow \chi) \rightarrow \psi \rightarrow \chi \)
syl6 l4 _
l7
cbv1 l0 l1 l2 l3 _
l8
cbv2.2
l9
cbv2.1
l10
cbv2.4
l11
cbv2.3
l12
equcomi
\( \vdash y = x \rightarrow x = y \)
l13
cbv2.5
\( \vdash \varphi \rightarrow x = y \rightarrow (\psi \leftrightarrow \chi) \)
biimpr
\( \vdash (\psi \leftrightarrow \chi) \rightarrow \chi \rightarrow \psi \)
syl56 l12 l13 _
cbv1 l8 l9 l10 l11 _
impbid l7 _