Theorem sbalv

Quantify with new variable inside substitution. (Contributed by NM, 18-Aug-1993.)

Hypothesis
sbalv.1
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash [ y' / x ] \, \forall z \, \varphi \leftrightarrow \forall z \, \psi \)
Proof
l0
sbal
\( \vdash [ y' / x ] \, \forall z \, \varphi \leftrightarrow \forall z \, [ y' / x ] \, \varphi \)
sbalv.1
albii _
\( \vdash \forall z \, [ y' / x ] \, \varphi \leftrightarrow \forall z \, \psi \)
bitri l0 _