Theorem cbvex2ivw

Description: One direction of cbvex2vw does not need a DV condition between x and y . Idea from relopabVD . (Contributed by SN, 27-Oct-2026)

	Ref	Expression
Hypothesis	cbvex2ivw.1	$$⊢\left(x=z\wedge y=w\right)\to \left(\phi \to \psi \right)$$
Assertion	cbvex2ivw	$$⊢\exists x\exists y\phi \to \exists z\exists w\psi$$

Proof

Step	Hyp	Ref	Expression
1		cbvex2ivw.1	$$⊢\left(x=z\wedge y=w\right)\to \left(\phi \to \psi \right)$$
2		ax6evr	$$⊢\exists zx=z$$
3		ax6evr	$$⊢\exists wy=w$$
4	1	ex	$$⊢x=z\to \left(y=w\to \left(\phi \to \psi \right)\right)$$
5	4	eximdv	$$⊢x=z\to \left(\exists wy=w\to \exists w\left(\phi \to \psi \right)\right)$$
6	3 5	mpi	$$⊢x=z\to \exists w\left(\phi \to \psi \right)$$
7		19.37v	$$⊢\exists w\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \exists w\psi \right)$$
8	6 7	sylib	$$⊢x=z\to \left(\phi \to \exists w\psi \right)$$
9	2 8	eximii	$$⊢\exists z\left(\phi \to \exists w\psi \right)$$
10	9	19.37iv	$$⊢\phi \to \exists z\exists w\psi$$
11	10	exlimivv	$$⊢\exists x\exists y\phi \to \exists z\exists w\psi$$