Theorem rexxfrd

Description: Transfer existential quantification from a variable x to another variable y contained in expression A . (Contributed by FL, 10-Apr-2007) (Revised by Mario Carneiro, 15-Aug-2014)

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

Proof

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