Theorem rexxfr

Description: Transfer existence from a variable x to another variable y contained in expression A . (Contributed by NM, 10-Jun-2005) (Revised by Mario Carneiro, 15-Aug-2014)

	Ref	Expression
Hypotheses	ralxfr.1	$$⊢y\in C\to A\in B$$
	ralxfr.2	$$⊢x\in B\to \exists y\in Cx=A$$
	ralxfr.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	rexxfr	$$⊢\exists x\in B\phi \leftrightarrow \exists y\in C\psi$$

Proof

Step	Hyp	Ref	Expression
1		ralxfr.1	$$⊢y\in C\to A\in B$$
2		ralxfr.2	$$⊢x\in B\to \exists y\in Cx=A$$
3		ralxfr.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
4		dfrex2	$$⊢\exists x\in B\phi \leftrightarrow \neg \forall x\in B\neg \phi$$
5		dfrex2	$$⊢\exists y\in C\psi \leftrightarrow \neg \forall y\in C\neg \psi$$
6	3	notbid	$$⊢x=A\to \left(\neg \phi \leftrightarrow \neg \psi \right)$$
7	1 2 6	ralxfr	$$⊢\forall x\in B\neg \phi \leftrightarrow \forall y\in C\neg \psi$$
8	5 7	xchbinxr	$$⊢\exists y\in C\psi \leftrightarrow \neg \forall x\in B\neg \phi$$
9	4 8	bitr4i	$$⊢\exists x\in B\phi \leftrightarrow \exists y\in C\psi$$