Theorem rexxfrd2

Description: Transfer existence from a variable x to another variable y contained in expression A . Variant of rexxfrd . (Contributed by Alexander van der Vekens, 25-Apr-2018)

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

Proof

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