Theorem 2moex

Double quantification with "at most one". Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker 2moexv when possible. (Contributed by NM, 3-Dec-2001.) (New usage is discouraged.)

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