Theorem cbvex2ivw 43455

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

Hypothesis

Ref	Expression
cbvex2ivw.1	⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 → 𝜓))

Assertion

Ref	Expression
cbvex2ivw	⊢ (∃𝑥∃𝑦𝜑 → ∃𝑧∃𝑤𝜓)

Distinct variable groups:   𝜑,𝑤,𝑧   𝑥,𝑤,𝑧   𝑦,𝑤,𝑧   𝜓,𝑥   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥, 𝑦)   𝜓(𝑧, 𝑤)

Proof of Theorem cbvex2ivw

Step	Hyp	Ref	Expression
1		ax6evr 2050	. . . 4 ⊢ ∃𝑧 𝑥 = 𝑧
2		ax6evr 2050	. . . . . 6 ⊢ ∃𝑤 𝑦 = 𝑤
3		cbvex2ivw.1	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 → 𝜓))
4	3	ex 418	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑦 = 𝑤 → (𝜑 → 𝜓)))
5	4	eximdv 1952	. . . . . 6 ⊢ (𝑥 = 𝑧 → (∃𝑤 𝑦 = 𝑤 → ∃𝑤(𝜑 → 𝜓)))
6	2, 5	mpi 21	. . . . 5 ⊢ (𝑥 = 𝑧 → ∃𝑤(𝜑 → 𝜓))
7		19.37v 2032	. . . . 5 ⊢ (∃𝑤(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑤𝜓))
8	6, 7	sylib 221	. . . 4 ⊢ (𝑥 = 𝑧 → (𝜑 → ∃𝑤𝜓))
9	1, 8	eximii 1870	. . 3 ⊢ ∃𝑧(𝜑 → ∃𝑤𝜓)
10	9	19.37iv 1983	. 2 ⊢ (𝜑 → ∃𝑧∃𝑤𝜓)
11	10	exlimivv 1967	1 ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑧∃𝑤𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by: (None)