Theorem rexlimddvcbvw 44195

Description: Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 44194. The equivalent of this theorem without the bound variable change is rexlimddv 3140. Version of rexlimddvcbv 44196 with a disjoint variable condition, which does not require ax-13 2370. (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 3216	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜃 ↔ ∃𝑦 ∈ 𝐴 𝜒)
4		rexlimddvcbvw.2	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓)
5	4	rexlimdvaa 3135	. . 3 ⊢ (𝜑 → (∃𝑦 ∈ 𝐴 𝜒 → 𝜓))
6	3, 5	biimtrid 242	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜃 → 𝜓))
7	1, 6	mpd 15	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-rex 3054

This theorem is referenced by:  mnuprdlem1  44261  mnuprdlem2  44262