Theorem 2moexv

Double quantification with "at most one". (Contributed by NM, 3-Dec-2001.)

Conclusion
\( \vdash \exists^\ast x \, \exists y \, \varphi \rightarrow \forall y \, \exists^\ast x \, \varphi \)
Proof
nfe1
l1
nfmov _
19.8a
moimi _
alrimi l1 _