Theorem rexlimddvcbvw 44794

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-clel 2840  df-rex 3090

This theorem is referenced by:  mnuprdlem1  44846  mnuprdlem2  44847