Step |
Hyp |
Ref |
Expression |
1 |
|
sb8eulem.nfsb |
|- F/ y [ w / x ] ph |
2 |
|
sb8v |
|- ( A. x ( ph <-> x = z ) <-> A. w [ w / x ] ( ph <-> x = z ) ) |
3 |
|
equsb3 |
|- ( [ w / x ] x = z <-> w = z ) |
4 |
3
|
sblbis |
|- ( [ w / x ] ( ph <-> x = z ) <-> ( [ w / x ] ph <-> w = z ) ) |
5 |
4
|
albii |
|- ( A. w [ w / x ] ( ph <-> x = z ) <-> A. w ( [ w / x ] ph <-> w = z ) ) |
6 |
|
nfv |
|- F/ y w = z |
7 |
1 6
|
nfbi |
|- F/ y ( [ w / x ] ph <-> w = z ) |
8 |
|
nfv |
|- F/ w ( [ y / x ] ph <-> y = z ) |
9 |
|
sbequ |
|- ( w = y -> ( [ w / x ] ph <-> [ y / x ] ph ) ) |
10 |
|
equequ1 |
|- ( w = y -> ( w = z <-> y = z ) ) |
11 |
9 10
|
bibi12d |
|- ( w = y -> ( ( [ w / x ] ph <-> w = z ) <-> ( [ y / x ] ph <-> y = z ) ) ) |
12 |
7 8 11
|
cbvalv1 |
|- ( A. w ( [ w / x ] ph <-> w = z ) <-> A. y ( [ y / x ] ph <-> y = z ) ) |
13 |
2 5 12
|
3bitri |
|- ( A. x ( ph <-> x = z ) <-> A. y ( [ y / x ] ph <-> y = z ) ) |
14 |
13
|
exbii |
|- ( E. z A. x ( ph <-> x = z ) <-> E. z A. y ( [ y / x ] ph <-> y = z ) ) |
15 |
|
eu6 |
|- ( E! x ph <-> E. z A. x ( ph <-> x = z ) ) |
16 |
|
eu6 |
|- ( E! y [ y / x ] ph <-> E. z A. y ( [ y / x ] ph <-> y = z ) ) |
17 |
14 15 16
|
3bitr4i |
|- ( E! x ph <-> E! y [ y / x ] ph ) |