Theorem rexxfr2d

Description: Transfer existential quantification from a variable x to another variable y contained in expression A . (Contributed by Mario Carneiro, 20-Aug-2014) (Proof shortened by Mario Carneiro, 19-Nov-2016)

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

Proof

Step	Hyp	Ref	Expression
1		ralxfr2d.1	$$⊢\left(\phi \wedge y\in C\right)\to A\in V$$
2		ralxfr2d.2	$$⊢\phi \to \left(x\in B\leftrightarrow \exists y\in Cx=A\right)$$
3		ralxfr2d.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	ralxfr2d	$$⊢\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)$$