Theorem rexlimddvcbvw 44218

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

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

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 2112

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2804  df-rex 3055

This theorem is referenced by:  mnuprdlem1  44284  mnuprdlem2  44285