Theorem rexlimddvcbv

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 . Usage of this theorem is discouraged because it depends on ax-13 , see rexlimddvcbvw for a weaker version that does not require it. (Contributed by Rohan Ridenour, 3-Aug-2023) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		rexlimddvcbv.1	$$⊢\phi \to \exists x\in A\theta$$
2		rexlimddvcbv.2	$$⊢\left(\phi \wedge \left(y\in A\wedge \chi \right)\right)\to \psi$$
3		rexlimddvcbv.3	$$⊢x=y\to \left(\theta \leftrightarrow \chi \right)$$
4	3 2	rexlimdvaacbv	$$⊢\phi \to \left(\exists x\in A\theta \to \psi \right)$$
5	1 4	mpd	$$⊢\phi \to \psi$$