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