Theorem cbvexdvaw 2049

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1548  ∃wex 1789

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790

This theorem is referenced by:  cbvex2vw  2051  isinf  9194  cbvoprab123vw  36537  cbvoprab13vw  36539  cbveudavw  36549  cbvopab1davw  36562  cbvopab2davw  36563  cbvopabdavw  36564  cbvoprab1davw  36569  cbvoprab2davw  36570  cbvoprab3davw  36571  cbvoprab123davw  36572  cbvoprab12davw  36573  cbvoprab23davw  36574  cbvoprab13davw  36575  dfttc4lem2  36827  bj-gabeqis  37361  grumnud  44800