Theorem cbvexdvaw 2047

Description: Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva 2409 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) (Revised by Gino Giotto, 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 321	. . . 4 ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (¬ 𝜓 ↔ ¬ 𝜒))
3	2	cbvaldvaw 2046	. . 3 ⊢ (𝜑 → (∀𝑥 ¬ 𝜓 ↔ ∀𝑦 ¬ 𝜒))
4		alnex 1789	. . 3 ⊢ (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
5		alnex 1789	. . 3 ⊢ (∀𝑦 ¬ 𝜒 ↔ ¬ ∃𝑦𝜒)
6	3, 4, 5	3bitr3g 316	. 2 ⊢ (𝜑 → (¬ ∃𝑥𝜓 ↔ ¬ ∃𝑦𝜒))
7	6	con4bid 320	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1541  ∃wex 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788

This theorem is referenced by:  cbvex2vw  2049  isinf  8891  bj-gabeqis  34863  grumnud  41577