Theorem cbv1
Rule used to change bound variables, using implicit substitution. Usage
of this theorem is discouraged because it depends on [ax-13]. See
cbv1v 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. (Revised by Wolf
Lammen, 13-May-2018.) (New usage is discouraged.)
Hypotheses
cbv1.1
\( \vdash \Finv x \, \varphi \)
cbv1.2
\( \vdash \Finv y \, \varphi \)
cbv1.3
\( \vdash \varphi \rightarrow \Finv y \, \psi \)
cbv1.4
\( \vdash \varphi \rightarrow \Finv x \, \chi \)
cbv1.5
\( \vdash \varphi \rightarrow x = y \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \forall x \, \psi \rightarrow \forall y \, \chi \)
Proof
l0
cbv1.2
cbv1.3
l2
nfim1 l0 _
l3
cbv1.1
cbv1.4
l5
nfim1 l3 _
cbv1.5
com12 _
a2d _
l9
cbv3 l2 l5 _
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \forall y \, (\varphi \rightarrow \chi) \)
cbv1.1
l11
19.21 _
\( \vdash \forall x \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow \forall x \, \psi \)
cbv1.2
19.21 _
\( \vdash \forall y \, (\varphi \rightarrow \chi) \leftrightarrow \varphi \rightarrow \forall y \, \chi \)
3imtr3i l9 l11 _
pm2.86i _