Theorem cbv2h
Rule used to change bound variables, using implicit substitution. Usage
of this theorem is discouraged because it depends on [ax-13].
(Contributed by NM, 11-May-1993.) (New usage is discouraged.)
Hypotheses
cbv2h.1
\( \vdash \varphi \rightarrow \psi \rightarrow \forall y \, \psi \)
cbv2h.2
\( \vdash \varphi \rightarrow \chi \rightarrow \forall x \, \chi \)
cbv2h.3
\( \vdash \varphi \rightarrow x = y \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \forall x \, \forall y \, \varphi \rightarrow (\forall x \, \psi \leftrightarrow \forall y \, \chi) \)
Proof
l0
cbv2h.1
l1
cbv2h.2
l2
cbv2h.3
\( \vdash \varphi \rightarrow x = y \rightarrow (\psi \leftrightarrow \chi) \)
biimp
\( \vdash (\psi \leftrightarrow \chi) \rightarrow \psi \rightarrow \chi \)
syl6 l2 _
l5
cbv1h l0 l1 _
l6
cbv2h.2
l7
cbv2h.1
l8
equcomi
\( \vdash y = x \rightarrow x = y \)
l9
cbv2h.3
\( \vdash \varphi \rightarrow x = y \rightarrow (\psi \leftrightarrow \chi) \)
biimpr
\( \vdash (\psi \leftrightarrow \chi) \rightarrow \chi \rightarrow \psi \)
syl56 l8 l9 _
cbv1h l6 l7 _
alcoms _
impbid l5 _