Theorem rexlimddvcbvw

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

	Ref	Expression
Hypotheses	rexlimddvcbvw.1	$$⊢\phi \to \exists x\in A\theta$$
	rexlimddvcbvw.2	$$⊢\left(\phi \wedge \left(y\in A\wedge \chi \right)\right)\to \psi$$
	rexlimddvcbvw.3	$$⊢x=y\to \left(\theta \leftrightarrow \chi \right)$$
Assertion	rexlimddvcbvw	$$⊢\phi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		rexlimddvcbvw.1	$$⊢\phi \to \exists x\in A\theta$$
2		rexlimddvcbvw.2	$$⊢\left(\phi \wedge \left(y\in A\wedge \chi \right)\right)\to \psi$$
3		rexlimddvcbvw.3	$$⊢x=y\to \left(\theta \leftrightarrow \chi \right)$$
4	3	cbvrexvw	$$⊢\exists x\in A\theta \leftrightarrow \exists y\in A\chi$$
5	2	rexlimdvaa	$$⊢\phi \to \left(\exists y\in A\chi \to \psi \right)$$
6	4 5	syl5bi	$$⊢\phi \to \left(\exists x\in A\theta \to \psi \right)$$
7	1 6	mpd	$$⊢\phi \to \psi$$