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\to \left(\psi \leftrightarrow \chi \right)$$
	rexxfr3d.x	$$⊢\phi \to \left(x\in A\leftrightarrow \exists y\in Bx=X\right)$$
	rexxfr3d.a	$$⊢\phi \to X\in V$$
Assertion	rexxfr3d	$$⊢\phi \to \left(\exists x\in A\psi \leftrightarrow \exists y\in B\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		rexxfr3d.s	$$⊢x=X\to \left(\psi \leftrightarrow \chi \right)$$
2		rexxfr3d.x	$$⊢\phi \to \left(x\in A\leftrightarrow \exists y\in Bx=X\right)$$
3		rexxfr3d.a	$$⊢\phi \to X\in V$$
4	3	adantr	$$⊢\left(\phi \wedge y\in B\right)\to X\in V$$
5	1	adantl	$$⊢\left(\phi \wedge x=X\right)\to \left(\psi \leftrightarrow \chi \right)$$
6	4 2 5	rexxfr2d	$$⊢\phi \to \left(\exists x\in A\psi \leftrightarrow \exists y\in B\chi \right)$$