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	|- ( ( E* x ph /\ A. x E* y ps ) -> E* y E. x ( ph /\ ps ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	|- F/ y ph
2		nfv	|- F/ y E* x ph
3		nfe1	|- F/ x E. x ( ph /\ ps )
4	3	nfmov	|- F/ x E* y E. x ( ph /\ ps )
5	1 2 4	moexexlem	|- ( ( E* x ph /\ A. x E* y ps ) -> E* y E. x ( ph /\ ps ) )