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 -> ( ph <-> ps ) )
Assertion	alxfr	|- ( ( A. y A e. B /\ A. x E. y x = A ) -> ( A. x ph <-> A. y ps ) )

Proof

Step	Hyp	Ref	Expression
1		alxfr.1	|- ( x = A -> ( ph <-> ps ) )
2	1	spcgv	|- ( A e. B -> ( A. x ph -> ps ) )
3	2	com12	|- ( A. x ph -> ( A e. B -> ps ) )
4	3	alimdv	|- ( A. x ph -> ( A. y A e. B -> A. y ps ) )
5	4	com12	|- ( A. y A e. B -> ( A. x ph -> A. y ps ) )
6	5	adantr	|- ( ( A. y A e. B /\ A. x E. y x = A ) -> ( A. x ph -> A. y ps ) )
7		nfa1	|- F/ y A. y ps
8		nfv	|- F/ y ph
9		sp	|- ( A. y ps -> ps )
10	9 1	syl5ibrcom	|- ( A. y ps -> ( x = A -> ph ) )
11	7 8 10	exlimd	|- ( A. y ps -> ( E. y x = A -> ph ) )
12	11	alimdv	|- ( A. y ps -> ( A. x E. y x = A -> A. x ph ) )
13	12	com12	|- ( A. x E. y x = A -> ( A. y ps -> A. x ph ) )
14	13	adantl	|- ( ( A. y A e. B /\ A. x E. y x = A ) -> ( A. y ps -> A. x ph ) )
15	6 14	impbid	|- ( ( A. y A e. B /\ A. x E. y x = A ) -> ( A. x ph <-> A. y ps ) )