Theorem moexexvw

Description: "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 Gino Giotto, 22-Aug-2023) Factor out common proof lines with moexex . (Revised by Wolf Lammen, 2-Oct-2023)

	Ref	Expression
Assertion	moexexvw	$$⊢\left({\exists }^{*}x\phi \wedge \forall x{\exists }^{*}y\psi \right)\to {\exists }^{*}y\exists x\left(\phi \wedge \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢Ⅎy\phi$$
2		nfv	$$⊢Ⅎy{\exists }^{*}x\phi$$
3		nfe1	$$⊢Ⅎx\exists x\left(\phi \wedge \psi \right)$$
4	3	nfmov	$$⊢Ⅎx{\exists }^{*}y\exists x\left(\phi \wedge \psi \right)$$
5	1 2 4	moexexlem	$$⊢\left({\exists }^{*}x\phi \wedge \forall x{\exists }^{*}y\psi \right)\to {\exists }^{*}y\exists x\left(\phi \wedge \psi \right)$$