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	|- ( ( x = z /\ y = w ) -> ( ph -> ps ) )
Assertion	cbvex2ivw	|- ( E. x E. y ph -> E. z E. w ps )

Proof

Step	Hyp	Ref	Expression
1		cbvex2ivw.1	|- ( ( x = z /\ y = w ) -> ( ph -> ps ) )
2		ax6evr	|- E. z x = z
3		ax6evr	|- E. w y = w
4	1	ex	|- ( x = z -> ( y = w -> ( ph -> ps ) ) )
5	4	eximdv	|- ( x = z -> ( E. w y = w -> E. w ( ph -> ps ) ) )
6	3 5	mpi	|- ( x = z -> E. w ( ph -> ps ) )
7		19.37v	|- ( E. w ( ph -> ps ) <-> ( ph -> E. w ps ) )
8	6 7	sylib	|- ( x = z -> ( ph -> E. w ps ) )
9	2 8	eximii	|- E. z ( ph -> E. w ps )
10	9	19.37iv	|- ( ph -> E. z E. w ps )
11	10	exlimivv	|- ( E. x E. y ph -> E. z E. w ps )