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 -> ( ps <-> th ) )
	rexlimdvaacbv.2	|- ( ( ph /\ ( y e. A /\ th ) ) -> ch )
Assertion	rexlimdvaacbv	|- ( ph -> ( E. x e. A ps -> ch ) )

Proof

Step	Hyp	Ref	Expression
1		rexlimdvaacbv.1	|- ( x = y -> ( ps <-> th ) )
2		rexlimdvaacbv.2	|- ( ( ph /\ ( y e. A /\ th ) ) -> ch )
3	1	cbvrexv	|- ( E. x e. A ps <-> E. y e. A th )
4	2	rexlimdvaa	|- ( ph -> ( E. y e. A th -> ch ) )
5	3 4	syl5bi	|- ( ph -> ( E. x e. A ps -> ch ) )