Theorem sbmo
Substitution into an at-most-one quantifier. (Contributed by Jeff
Madsen, 2-Sep-2009.)
Conclusion
\( \vdash [ y' / x ] \, \exists^\ast z \, \varphi \leftrightarrow \exists^\ast z \, [ y' / x ] \, \varphi \)
Proof
l0
sbex
\( \vdash [ y' / x ] \, \exists w \, \forall z \, (\varphi \rightarrow z = w) \leftrightarrow \exists w \, [ y' / x ] \, \forall z \, (\varphi \rightarrow z = w) \)
nfv
sblim _
sbalv _
exbii _
\( \vdash \exists w \, [ y' / x ] \, \forall z \, (\varphi \rightarrow z = w) \leftrightarrow \exists w \, \forall z \, ([ y' / x ] \, \varphi \rightarrow z = w) \)
l5
bitri l0 _
\( \vdash [ y' / x ] \, \exists w \, \forall z \, (\varphi \rightarrow z = w) \leftrightarrow \exists w \, \forall z \, ([ y' / x ] \, \varphi \rightarrow z = w) \)
dfmo
l7
sbbii _
\( \vdash [ y' / x ] \, \exists^\ast z \, \varphi \leftrightarrow [ y' / x ] \, \exists w \, \forall z \, (\varphi \rightarrow z = w) \)
dfmo
\( \vdash \exists^\ast z \, [ y' / x ] \, \varphi \leftrightarrow \exists w \, \forall z \, ([ y' / x ] \, \varphi \rightarrow z = w) \)
3bitr4i l5 l7 _