Theorem alxfr

Description: Transfer universal quantification from a variable x to another variable y contained in expression A . (Contributed by NM, 18-Feb-2007)

	Ref	Expression
Hypothesis	alxfr.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	alxfr	$$⊢\left(\forall yA\in B\wedge \forall x\exists yx=A\right)\to \left(\forall x\phi \leftrightarrow \forall y\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		alxfr.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2	1	spcgv	$$⊢A\in B\to \left(\forall x\phi \to \psi \right)$$
3	2	com12	$$⊢\forall x\phi \to \left(A\in B\to \psi \right)$$
4	3	alimdv	$$⊢\forall x\phi \to \left(\forall yA\in B\to \forall y\psi \right)$$
5	4	com12	$$⊢\forall yA\in B\to \left(\forall x\phi \to \forall y\psi \right)$$
6	5	adantr	$$⊢\left(\forall yA\in B\wedge \forall x\exists yx=A\right)\to \left(\forall x\phi \to \forall y\psi \right)$$
7		nfa1	$$⊢Ⅎy\forall y\psi$$
8		nfv	$$⊢Ⅎy\phi$$
9		sp	$$⊢\forall y\psi \to \psi$$
10	9 1	syl5ibrcom	$$⊢\forall y\psi \to \left(x=A\to \phi \right)$$
11	7 8 10	exlimd	$$⊢\forall y\psi \to \left(\exists yx=A\to \phi \right)$$
12	11	alimdv	$$⊢\forall y\psi \to \left(\forall x\exists yx=A\to \forall x\phi \right)$$
13	12	com12	$$⊢\forall x\exists yx=A\to \left(\forall y\psi \to \forall x\phi \right)$$
14	13	adantl	$$⊢\left(\forall yA\in B\wedge \forall x\exists yx=A\right)\to \left(\forall y\psi \to \forall x\phi \right)$$
15	6 14	impbid	$$⊢\left(\forall yA\in B\wedge \forall x\exists yx=A\right)\to \left(\forall x\phi \leftrightarrow \forall y\psi \right)$$