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

Proof

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