Theorem moexex

"At most one" double quantification. Usage of this theorem is discouraged because it depends on [ax-13]. Use the version moexexvw when possible. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Wolf Lammen, 28-Dec-2018.) Factor out common proof lines with moexexvw. (Revised by Wolf Lammen, 2-Oct-2023.) (New usage is discouraged.)

Hypothesis
moexex.1
\( \vdash \Finv y \, \varphi \)
Conclusion
\( \vdash \exists^\ast x \, \varphi \wedge \forall x \, \exists^\ast y \, \psi \rightarrow \exists^\ast y \, \exists x \, (\varphi \wedge \psi) \)
Proof
l0
moexex.1
moexex.1
l2
nfmo _
nfe1
nfmo _
moexexlem l0 l2 _