Theorem rexlimdvaacbv

Description: Unpack a restricted existential antecedent while changing the variable with implicit substitution. The equivalent of this theorem without the bound variable change is rexlimdvaa . (Contributed by Rohan Ridenour, 3-Aug-2023)

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

Proof

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