Theorem 2eumo

Nested unique existential quantifier and at-most-one quantifier. (Contributed by NM, 3-Dec-2001.)

Conclusion
\( \vdash \exists{!} x \, \exists^\ast y \, \varphi \rightarrow \exists^\ast x \, \exists{!} y \, \varphi \)
Proof
l0
euimmo
\( \vdash \forall x \, (\exists{!} y \, \varphi \rightarrow \exists^\ast y \, \varphi) \rightarrow \exists{!} x \, \exists^\ast y \, \varphi \rightarrow \exists^\ast x \, \exists{!} y \, \varphi \)
eumo
\( \vdash \exists{!} y \, \varphi \rightarrow \exists^\ast y \, \varphi \)
mpg l0 _