Theorem moaneu

Nested at-most-one and unique existential quantifiers. (Contributed by NM, 25-Jan-2006.) (Proof shortened by Wolf Lammen, 27-Dec-2018.)

Conclusion
\( \vdash \exists^\ast x \, (\varphi \wedge \exists{!} x \, \varphi) \)
Proof
l0
moanmo
\( \vdash \exists^\ast x \, (\varphi \wedge \exists^\ast x \, \varphi) \)
eumo
anim2i _
moimi _
\( \vdash \exists^\ast x \, (\varphi \wedge \exists^\ast x \, \varphi) \rightarrow \exists^\ast x \, (\varphi \wedge \exists{!} x \, \varphi) \)
ax-mp l0 _