Theorem ralxfr

Description: Transfer universal quantification 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	ralxfr	$$⊢\forall x\in B\phi \leftrightarrow \forall 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	1	adantl	$$⊢\left(\top \wedge y\in C\right)\to A\in B$$
5	2	adantl	$$⊢\left(\top \wedge x\in B\right)\to \exists y\in Cx=A$$
6	3	adantl	$$⊢\left(\top \wedge x=A\right)\to \left(\phi \leftrightarrow \psi \right)$$
7	4 5 6	ralxfrd	$$⊢\top \to \left(\forall x\in B\phi \leftrightarrow \forall y\in C\psi \right)$$
8	7	mptru	$$⊢\forall x\in B\phi \leftrightarrow \forall y\in C\psi$$