| Step |
Hyp |
Ref |
Expression |
| 1 |
|
nf5 |
|- ( F/ y ph <-> A. y ( ph -> A. y ph ) ) |
| 2 |
1
|
biimpi |
|- ( F/ y ph -> A. y ( ph -> A. y ph ) ) |
| 3 |
2
|
alimi |
|- ( A. x F/ y ph -> A. x A. y ( ph -> A. y ph ) ) |
| 4 |
|
nfa2 |
|- F/ y A. x A. y ( ph -> A. y ph ) |
| 5 |
|
bj-hbext |
|- ( A. x A. y ( ph -> A. y ph ) -> ( E. x ph -> A. y E. x ph ) ) |
| 6 |
4 5
|
alrimi |
|- ( A. x A. y ( ph -> A. y ph ) -> A. y ( E. x ph -> A. y E. x ph ) ) |
| 7 |
3 6
|
syl |
|- ( A. x F/ y ph -> A. y ( E. x ph -> A. y E. x ph ) ) |
| 8 |
|
nf5 |
|- ( F/ y E. x ph <-> A. y ( E. x ph -> A. y E. x ph ) ) |
| 9 |
7 8
|
sylibr |
|- ( A. x F/ y ph -> F/ y E. x ph ) |