Theorem cbvexdvaw 2037

Description: Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva 2414 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid ax-13 2376. (Revised by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by Wolf Lammen, 10-Feb-2024.)

Hypothesis

Ref	Expression
cbvaldvaw.1	⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
cbvexdvaw	⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))

Distinct variable groups:   𝜓,𝑦   𝜒,𝑥   𝜑,𝑥,𝑦

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑦)

Proof of Theorem cbvexdvaw

Step	Hyp	Ref	Expression
1		cbvaldvaw.1	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))
2	1	notbid 318	. . . 4 ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (¬ 𝜓 ↔ ¬ 𝜒))
3	2	cbvaldvaw 2036	. . 3 ⊢ (𝜑 → (∀𝑥 ¬ 𝜓 ↔ ∀𝑦 ¬ 𝜒))
4		alnex 1780	. . 3 ⊢ (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
5		alnex 1780	. . 3 ⊢ (∀𝑦 ¬ 𝜒 ↔ ¬ ∃𝑦𝜒)
6	3, 4, 5	3bitr3g 313	. 2 ⊢ (𝜑 → (¬ ∃𝑥𝜓 ↔ ¬ ∃𝑦𝜒))
7	6	con4bid 317	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1537  ∃wex 1778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779

This theorem is referenced by:  cbvex2vw  2039  isinf  9297  isinfOLD  9298  cbvoprab123vw  36241  cbvoprab13vw  36243  cbveudavw  36253  cbvopab1davw  36266  cbvopab2davw  36267  cbvopabdavw  36268  cbvoprab1davw  36273  cbvoprab2davw  36274  cbvoprab3davw  36275  cbvoprab123davw  36276  cbvoprab12davw  36277  cbvoprab23davw  36278  cbvoprab13davw  36279  bj-gabeqis  36940  grumnud  44310