Theorem rexlimddvcbvw 45280

Description: Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 45279. The equivalent of this theorem without the bound variable change is rexlimddv 3169. Version of rexlimddvcbv 45281 with a disjoint variable condition, which does not require ax-13 2401. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Revised by GG, 2-Apr-2024.)

Hypotheses

Ref	Expression
rexlimddvcbvw.1	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃)
rexlimddvcbvw.2	⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓)
rexlimddvcbvw.3	⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒))

Assertion

Ref	Expression
rexlimddvcbvw	⊢ (𝜑 → 𝜓)

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

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

Proof of Theorem rexlimddvcbvw

Step	Hyp	Ref	Expression
1		rexlimddvcbvw.1	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃)
2		rexlimddvcbvw.3	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒))
3	2	cbvrexvw 3241	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜃 ↔ ∃𝑦 ∈ 𝐴 𝜒)
4		rexlimddvcbvw.2	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓)
5	4	rexlimdvaa 3164	. . 3 ⊢ (𝜑 → (∃𝑦 ∈ 𝐴 𝜒 → 𝜓))
6	3, 5	biimtrid 245	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜃 → 𝜓))
7	1, 6	mpd 16	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2144  ∃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-rex 3087

This theorem is used by:  mnuprdlem1  45332  mnuprdlem2  45333