Theorem cbvrexdva 3217

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 2123, ax-ext 2708. (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 318	. . . 4 ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (¬ 𝜓 ↔ ¬ 𝜒))
3	2	cbvraldva 3216	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜒))
4		ralnex 3062	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜓)
5		ralnex 3062	. . 3 ⊢ (∀𝑦 ∈ 𝐴 ¬ 𝜒 ↔ ¬ ∃𝑦 ∈ 𝐴 𝜒)
6	3, 4, 5	3bitr3g 313	. 2 ⊢ (𝜑 → (¬ ∃𝑥 ∈ 𝐴 𝜓 ↔ ¬ ∃𝑦 ∈ 𝐴 𝜒))
7	6	con4bid 317	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐴 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wral 3051  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2811  df-ral 3052  df-rex 3061

This theorem is referenced by:  tfrlem3a  8308  2sqmo  27404  trgcopy  28876  trgcopyeu  28878  acopyeu  28906  tgasa1  28930  dispcmp  34016  satffunlem1lem1  35596  satffunlem2lem1  35598  cbviundavw  36456  f1omptsn  37538  pibt2  37618  prjsprel  42843  opnneilem  49147