Theorem cbvexdvaw 2039

Description: Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva 2408 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid ax-13 2370. (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 2038	. . 3 ⊢ (𝜑 → (∀𝑥 ¬ 𝜓 ↔ ∀𝑦 ¬ 𝜒))
4		alnex 1781	. . 3 ⊢ (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
5		alnex 1781	. . 3 ⊢ (∀𝑦 ¬ 𝜒 ↔ ¬ ∃𝑦𝜒)
6	3, 4, 5	3bitr3g 313	. 2 ⊢ (𝜑 → (¬ ∃𝑥𝜓 ↔ ¬ ∃𝑦𝜒))
7	6	con4bid 317	1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

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

This theorem is referenced by:  cbvex2vw  2041  isinf  9154  cbvoprab123vw  36233  cbvoprab13vw  36235  cbveudavw  36245  cbvopab1davw  36258  cbvopab2davw  36259  cbvopabdavw  36260  cbvoprab1davw  36265  cbvoprab2davw  36266  cbvoprab3davw  36267  cbvoprab123davw  36268  cbvoprab12davw  36269  cbvoprab23davw  36270  cbvoprab13davw  36271  bj-gabeqis  36932  grumnud  44279