Theorem cbv1v
Rule used to change bound variables, using implicit substitution.
Version of cbv1 with a disjoint variable condition, which does not
require [ax-13]. (Contributed by NM, 5-Aug-1993.) (Revised by BJ,
16-Jun-2019.)
Hypotheses
cbv1v.1
\( \vdash \Finv x \, \varphi \)
cbv1v.2
\( \vdash \Finv y \, \varphi \)
cbv1v.3
\( \vdash \varphi \rightarrow \Finv y \, \psi \)
cbv1v.4
\( \vdash \varphi \rightarrow \Finv x \, \chi \)
cbv1v.5
\( \vdash \varphi \rightarrow x = y \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \forall x \, \psi \rightarrow \forall y \, \chi \)
Proof
l0
cbv1v.2
cbv1v.3
l2
nfim1 l0 _
l3
cbv1v.1
cbv1v.4
l5
nfim1 l3 _
cbv1v.5
com12 _
a2d _
l9
cbv3v l2 l5 _
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \forall y \, (\varphi \rightarrow \chi) \)
cbv1v.1
l11
19.21 _
\( \vdash \forall x \, (\varphi \rightarrow \psi) \leftrightarrow \varphi \rightarrow \forall x \, \psi \)
cbv1v.2
19.21 _
\( \vdash \forall y \, (\varphi \rightarrow \chi) \leftrightarrow \varphi \rightarrow \forall y \, \chi \)
3imtr3i l9 l11 _
pm2.86i _