Theorem ralxfr2d

Description: Transfer universal quantification from a variable x to another variable y contained in expression A . (Contributed by Mario Carneiro, 20-Aug-2014)

	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	ralxfr2d	$$⊢\phi \to \left(\forall x\in B\psi \leftrightarrow \forall 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		elisset	$$⊢A\in V\to \exists xx=A$$
5	1 4	syl	$$⊢\left(\phi \wedge y\in C\right)\to \exists xx=A$$
6	2	biimprd	$$⊢\phi \to \left(\exists y\in Cx=A\to x\in B\right)$$
7		r19.23v	$$⊢\forall y\in C\left(x=A\to x\in B\right)\leftrightarrow \left(\exists y\in Cx=A\to x\in B\right)$$
8	6 7	sylibr	$$⊢\phi \to \forall y\in C\left(x=A\to x\in B\right)$$
9	8	r19.21bi	$$⊢\left(\phi \wedge y\in C\right)\to \left(x=A\to x\in B\right)$$
10		eleq1	$$⊢x=A\to \left(x\in B\leftrightarrow A\in B\right)$$
11	9 10	mpbidi	$$⊢\left(\phi \wedge y\in C\right)\to \left(x=A\to A\in B\right)$$
12	11	exlimdv	$$⊢\left(\phi \wedge y\in C\right)\to \left(\exists xx=A\to A\in B\right)$$
13	5 12	mpd	$$⊢\left(\phi \wedge y\in C\right)\to A\in B$$
14	2	biimpa	$$⊢\left(\phi \wedge x\in B\right)\to \exists y\in Cx=A$$
15	13 14 3	ralxfrd	$$⊢\phi \to \left(\forall x\in B\psi \leftrightarrow \forall y\in C\chi \right)$$