Theorem cbvrexdva 3242

Description: Rule used to change the bound variable in a restricted existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) Avoid ax-9 2151, ax-ext 2733. (Revised by Wolf Lammen, 9-Mar-2025.)

Hypothesis

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

Assertion

Ref	Expression
cbvrexdva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐴 𝜒))

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

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

Proof of Theorem cbvrexdva

Step	Hyp	Ref	Expression
1		cbvraldva.1	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))
2	1	notbid 320	. . . 4 ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (¬ 𝜓 ↔ ¬ 𝜒))
3	2	cbvraldva 3241	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜒))
4		ralnex 3087	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜓)
5		ralnex 3087	. . 3 ⊢ (∀𝑦 ∈ 𝐴 ¬ 𝜒 ↔ ¬ ∃𝑦 ∈ 𝐴 𝜒)
6	3, 4, 5	3bitr3g 315	. 2 ⊢ (𝜑 → (¬ ∃𝑥 ∈ 𝐴 𝜓 ↔ ¬ ∃𝑦 ∈ 𝐴 𝜒))
7	6	con4bid 319	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐴 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399  ∀wral 3075  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-clel 2836  df-ral 3076  df-rex 3086

This theorem is referenced by:  tfrlem3a  8342  2sqmo  27478  trgcopy  28950  trgcopyeu  28952  acopyeu  28980  tgasa1  29004  dispcmp  34117  satffunlem1lem1  35716  satffunlem2lem1  35718  cbviundavw  36586  f1omptsn  37795  pibt2  37875  prjsprel  43150  opnneilem  49491