Theorem sbex
Move existential quantifier in and out of substitution. (Contributed by
NM, 27-Sep-2003.)
Conclusion
\( \vdash [ z' / y ] \, \exists x \, \varphi \leftrightarrow \exists x \, [ z' / y ] \, \varphi \)
Proof
l0
sbn
\( \vdash [ z' / y ] \, (\neg \forall x \, \neg \varphi) \leftrightarrow \neg [ z' / y ] \, \forall x \, \neg \varphi \)
sbn
sbalv _
\( \vdash [ z' / y ] \, \forall x \, \neg \varphi \leftrightarrow \forall x \, \neg [ z' / y ] \, \varphi \)
l3
xchbinx l0 _
\( \vdash [ z' / y ] \, (\neg \forall x \, \neg \varphi) \leftrightarrow \neg \forall x \, \neg [ z' / y ] \, \varphi \)
df-ex
l5
sbbii _
\( \vdash [ z' / y ] \, \exists x \, \varphi \leftrightarrow [ z' / y ] \, (\neg \forall x \, \neg \varphi) \)
df-ex
\( \vdash \exists x \, [ z' / y ] \, \varphi \leftrightarrow \neg \forall x \, \neg [ z' / y ] \, \varphi \)
3bitr4i l3 l5 _