Theorem moexexv

"At most one" double quantification. Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker moexexvw when possible. (Contributed by NM, 26-Jan-1997.) (New usage is discouraged.)

Conclusion

\( \vdash \exists^\ast x \, \varphi \wedge \forall x \, \exists^\ast y \, \psi \rightarrow \exists^\ast y \, \exists x \, (\varphi \wedge \psi) \)

Proof

nfv

moexex _