Theorem moexexvw

"At most one" double quantification. Version of moexexv with an additional disjoint variable condition, which does not require [ax-13]. (Contributed by NM, 26-Jan-1997.) (Revised by GG, 22-Aug-2023.) Factor out common proof lines with moexex. (Revised by Wolf Lammen, 2-Oct-2023.)

Conclusion
\( \vdash \exists^\ast x \, \varphi \wedge \forall x \, \exists^\ast y \, \psi \rightarrow \exists^\ast y \, \exists x \, (\varphi \wedge \psi) \)
Proof
l0
nfv
l1
nfv
nfe1
nfmov _
moexexlem l0 l1 _