Theorem sb9

Commutation of quantification and substitution variables. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 5-Aug-1993.) Allow a shortening of sb9i. (Revised by Wolf Lammen, 15-Jun-2019.) (New usage is discouraged.)

Conclusion
\( \vdash \forall x \, [ x / y ] \, \varphi \leftrightarrow \forall y \, [ y / x ] \, \varphi \)
Proof
l0
nfs1v
\( \vdash \Finv y \, [ x / y ] \, \varphi \)
l1
sb8 _
l2
sbco
\( \vdash [ y / x ] \, [ x / y ] \, \varphi \leftrightarrow [ y / x ] \, \varphi \)
l3
albii _
l4
bitri l1 _