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	⊢ ( ( ∃* 𝑥 𝜑 ∧ ∀ 𝑥 ∃* 𝑦 𝜓 ) → ∃* 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑦 𝜑
2		nfv	⊢ Ⅎ 𝑦 ∃* 𝑥 𝜑
3		nfe1	⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝜑 ∧ 𝜓 )
4	3	nfmov	⊢ Ⅎ 𝑥 ∃* 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝜓 )
5	1 2 4	moexexlem	⊢ ( ( ∃* 𝑥 𝜑 ∧ ∀ 𝑥 ∃* 𝑦 𝜓 ) → ∃* 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) )