Theorem rexlimddvcbv 44248

Description: Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 44246. The equivalent of this theorem without the bound variable change is rexlimddv 3139. Usage of this theorem is discouraged because it depends on ax-13 2372, see rexlimddvcbvw 44247 for a weaker version that does not require it. (Contributed by Rohan Ridenour, 3-Aug-2023.) (New usage is discouraged.)

Hypotheses

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

Assertion

Ref	Expression
rexlimddvcbv	⊢ (𝜑 → 𝜓)

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

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

Proof of Theorem rexlimddvcbv

Step	Hyp	Ref	Expression
1		rexlimddvcbv.1	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜃)
2		rexlimddvcbv.3	. . 3 ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜒))
3		rexlimddvcbv.2	. . 3 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝜒)) → 𝜓)
4	2, 3	rexlimdvaacbv 44246	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜃 → 𝜓))
5	1, 4	mpd 15	1 ⊢ (𝜑 → 𝜓)

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

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 2113  ax-10 2144  ax-11 2160  ax-12 2180  ax-13 2372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057

This theorem is referenced by: (None)