Theorem sb8mo
Variable substitution for the at-most-one quantifier. Usage of this
theorem is discouraged because it depends on [ax-13]. (Contributed by
Alexander van der Vekens, 17-Jun-2017.) (New usage is discouraged.)
Hypothesis
sb8eu.1
\( \vdash \Finv y \, \varphi \)
Conclusion
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists^\ast y \, [ y / x ] \, \varphi \)
Proof
sb8eu.1
l1
sb8e _
sb8eu.1
sb8eu _
l4
imbi12i l1 _
\( \vdash \exists x \, \varphi \rightarrow \exists{!} x \, \varphi \leftrightarrow \exists y \, [ y / x ] \, \varphi \rightarrow \exists{!} y \, [ y / x ] \, \varphi \)
l5
moeu
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists x \, \varphi \rightarrow \exists{!} x \, \varphi \)
moeu
\( \vdash \exists^\ast y \, [ y / x ] \, \varphi \leftrightarrow \exists y \, [ y / x ] \, \varphi \rightarrow \exists{!} y \, [ y / x ] \, \varphi \)
3bitr4i l4 l5 _