This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )