Theorem cbvrexdva 3243

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 2154, ax-ext 2732. (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 321	. . . 4 ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (¬ 𝜓 ↔ ¬ 𝜒))
3	2	cbvraldva 3242	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜒))
4		ralnex 3088	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜓)
5		ralnex 3088	. . 3 ⊢ (∀𝑦 ∈ 𝐴 ¬ 𝜒 ↔ ¬ ∃𝑦 ∈ 𝐴 𝜒)
6	3, 4, 5	3bitr3g 316	. 2 ⊢ (𝜑 → (¬ ∃𝑥 ∈ 𝐴 𝜓 ↔ ¬ ∃𝑦 ∈ 𝐴 𝜒))
7	6	con4bid 320	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐴 𝜒))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wral 3076  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835  df-ral 3077  df-rex 3087

This theorem is used by:  tfrlem3a  8388  2sqmo  27770  trgcopy  29317  trgcopyeu  29319  acopyeu  29348  tgasa1  29409  tgextahpl  33075  tgextancgra  33080  dispcmp  34538  satffunlem1lem1  36254  satffunlem2lem1  36256  cbviundavw  37144  f1omptsn  38354  pibt2  38434  prjsprel  43726  opnneilem  50114