Step |
Hyp |
Ref |
Expression |
1 |
|
nfnf1 |
|- F/ y F/ y ph |
2 |
1
|
nfal |
|- F/ y A. x F/ y ph |
3 |
|
equsb3 |
|- ( [ v / x ] x = u <-> v = u ) |
4 |
3
|
sblbis |
|- ( [ v / x ] ( ph <-> x = u ) <-> ( [ v / x ] ph <-> v = u ) ) |
5 |
|
nfa1 |
|- F/ x A. x F/ y ph |
6 |
|
sp |
|- ( A. x F/ y ph -> F/ y ph ) |
7 |
5 6
|
nfsbd |
|- ( A. x F/ y ph -> F/ y [ v / x ] ph ) |
8 |
|
nfvd |
|- ( A. x F/ y ph -> F/ y v = u ) |
9 |
7 8
|
nfbid |
|- ( A. x F/ y ph -> F/ y ( [ v / x ] ph <-> v = u ) ) |
10 |
4 9
|
nfxfrd |
|- ( A. x F/ y ph -> F/ y [ v / x ] ( ph <-> x = u ) ) |
11 |
|
sbequ |
|- ( v = y -> ( [ v / x ] ( ph <-> x = u ) <-> [ y / x ] ( ph <-> x = u ) ) ) |
12 |
11
|
a1i |
|- ( A. x F/ y ph -> ( v = y -> ( [ v / x ] ( ph <-> x = u ) <-> [ y / x ] ( ph <-> x = u ) ) ) ) |
13 |
2 10 12
|
cbvald |
|- ( A. x F/ y ph -> ( A. v [ v / x ] ( ph <-> x = u ) <-> A. y [ y / x ] ( ph <-> x = u ) ) ) |
14 |
|
nfv |
|- F/ v ( ph <-> x = u ) |
15 |
14
|
sb8 |
|- ( A. x ( ph <-> x = u ) <-> A. v [ v / x ] ( ph <-> x = u ) ) |
16 |
15
|
bicomi |
|- ( A. v [ v / x ] ( ph <-> x = u ) <-> A. x ( ph <-> x = u ) ) |
17 |
|
equsb3 |
|- ( [ y / x ] x = u <-> y = u ) |
18 |
17
|
sblbis |
|- ( [ y / x ] ( ph <-> x = u ) <-> ( [ y / x ] ph <-> y = u ) ) |
19 |
18
|
albii |
|- ( A. y [ y / x ] ( ph <-> x = u ) <-> A. y ( [ y / x ] ph <-> y = u ) ) |
20 |
13 16 19
|
3bitr3g |
|- ( A. x F/ y ph -> ( A. x ( ph <-> x = u ) <-> A. y ( [ y / x ] ph <-> y = u ) ) ) |
21 |
20
|
exbidv |
|- ( A. x F/ y ph -> ( E. u A. x ( ph <-> x = u ) <-> E. u A. y ( [ y / x ] ph <-> y = u ) ) ) |
22 |
|
eu6 |
|- ( E! x ph <-> E. u A. x ( ph <-> x = u ) ) |
23 |
|
eu6 |
|- ( E! y [ y / x ] ph <-> E. u A. y ( [ y / x ] ph <-> y = u ) ) |
24 |
21 22 23
|
3bitr4g |
|- ( A. x F/ y ph -> ( E! x ph <-> E! y [ y / x ] ph ) ) |