Theorem sbal
Move universal quantifier in and out of substitution. (Contributed by
NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.)
Reduce dependencies on axioms. (Revised by Steven Nguyen,
13-Aug-2023.)
Conclusion
\( \vdash [ z' / y ] \, \forall x \, \varphi \leftrightarrow \forall x \, [ z' / y ] \, \varphi \)
Proof
l0
alcom
\( \vdash \forall w \, \forall x \, (w = z' \rightarrow \forall y \, (y = w \rightarrow \varphi)) \leftrightarrow \forall x \, \forall w \, (w = z' \rightarrow \forall y \, (y = w \rightarrow \varphi)) \)
19.21v
l2
albii _
\( \vdash \forall y \, \forall x \, (y = w \rightarrow \varphi) \leftrightarrow \forall y \, (y = w \rightarrow \forall x \, \varphi) \)
alcom
\( \vdash \forall y \, \forall x \, (y = w \rightarrow \varphi) \leftrightarrow \forall x \, \forall y \, (y = w \rightarrow \varphi) \)
bitr3i l2 _
imbi2i _
l6
albii _
\( \vdash \forall w \, (w = z' \rightarrow \forall y \, (y = w \rightarrow \forall x \, \varphi)) \leftrightarrow \forall w \, (w = z' \rightarrow \forall x \, \forall y \, (y = w \rightarrow \varphi)) \)
l7
dfsb
\( \vdash [ z' / y ] \, \forall x \, \varphi \leftrightarrow \forall w \, (w = z' \rightarrow \forall y \, (y = w \rightarrow \forall x \, \varphi)) \)
19.21v
albii _
\( \vdash \forall w \, \forall x \, (w = z' \rightarrow \forall y \, (y = w \rightarrow \varphi)) \leftrightarrow \forall w \, (w = z' \rightarrow \forall x \, \forall y \, (y = w \rightarrow \varphi)) \)
l10
3bitr4i l6 l7 _
\( \vdash [ z' / y ] \, \forall x \, \varphi \leftrightarrow \forall w \, \forall x \, (w = z' \rightarrow \forall y \, (y = w \rightarrow \varphi)) \)
dfsb
albii _
\( \vdash \forall x \, [ z' / y ] \, \varphi \leftrightarrow \forall x \, \forall w \, (w = z' \rightarrow \forall y \, (y = w \rightarrow \varphi)) \)
3bitr4i l0 l10 _