Theorem cbv3v

Rule used to change bound variables, using implicit substitution. Version of cbv3 with a disjoint variable condition, which does not require [ax-13]. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.)

Hypotheses
cbv3v.nf1
\( \vdash \Finv y \, \varphi \)
cbv3v.nf2
\( \vdash \Finv x \, \psi \)
cbv3v.1
\( \vdash x = y \rightarrow \varphi \rightarrow \psi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \forall y \, \psi \)
Proof
cbv3v.nf1
nf5ri _
l2
hbal _
l3
cbv3v.nf2
\( \vdash \Finv x \, \psi \)
cbv3v.1
\( \vdash x = y \rightarrow \varphi \rightarrow \psi \)
spimfv l3 _
alrimih l2 _