Theorem rexxfr3d

Description: Transfer existential quantification from a variable x to another variable y contained in expression A . (Contributed by SN, 20-Jun-2025)

	Ref	Expression
Hypotheses	rexxfr3d.s	|- ( x = X -> ( ps <-> ch ) )
	rexxfr3d.x	|- ( ph -> ( x e. A <-> E. y e. B x = X ) )
	rexxfr3d.a	|- ( ph -> X e. V )
Assertion	rexxfr3d	|- ( ph -> ( E. x e. A ps <-> E. y e. B ch ) )

Proof

Step	Hyp	Ref	Expression
1		rexxfr3d.s	|- ( x = X -> ( ps <-> ch ) )
2		rexxfr3d.x	|- ( ph -> ( x e. A <-> E. y e. B x = X ) )
3		rexxfr3d.a	|- ( ph -> X e. V )
4	3	adantr	|- ( ( ph /\ y e. B ) -> X e. V )
5	1	adantl	|- ( ( ph /\ x = X ) -> ( ps <-> ch ) )
6	4 2 5	rexxfr2d	|- ( ph -> ( E. x e. A ps <-> E. y e. B ch ) )