Theorem cbvexdvaw 2039

Description: Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva 2415 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid ax-13 2377. (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  9273  isinfOLD  9274  cbvoprab123vw  36262  cbvoprab13vw  36264  cbveudavw  36274  cbvopab1davw  36287  cbvopab2davw  36288  cbvopabdavw  36289  cbvoprab1davw  36294  cbvoprab2davw  36295  cbvoprab3davw  36296  cbvoprab123davw  36297  cbvoprab12davw  36298  cbvoprab23davw  36299  cbvoprab13davw  36300  bj-gabeqis  36961  grumnud  44277