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

Proof

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