Theorem cbval2

Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker cbval2v if possible. (Contributed by NM, 22-Dec-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-Sep-2023.) (New usage is discouraged.)

Hypotheses
cbval2.1
\( \vdash \Finv z \, \varphi \)
cbval2.2
\( \vdash \Finv w \, \varphi \)
cbval2.3
\( \vdash \Finv x \, \psi \)
cbval2.4
\( \vdash \Finv y \, \psi \)
cbval2.5
\( \vdash x = z \wedge y = w \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \forall x \, \forall y \, \varphi \leftrightarrow \forall z \, \forall w \, \psi \)
Proof
cbval2.1
l1
nfal _
cbval2.3
l3
nfal _
l4
nfv
l5
nfv
cbval2.2
l7
a1i _
cbval2.4
l9
a1i _
cbval2.5
ex _
cbv2 l4 l5 l7 l9 _
cbval l1 l3 _