Step |
Hyp |
Ref |
Expression |
1 |
|
sb8iota.1 |
|- F/ y ph |
2 |
|
nfv |
|- F/ w ( ph <-> x = z ) |
3 |
2
|
sb8 |
|- ( A. x ( ph <-> x = z ) <-> A. w [ w / x ] ( ph <-> x = z ) ) |
4 |
|
sbbi |
|- ( [ w / x ] ( ph <-> x = z ) <-> ( [ w / x ] ph <-> [ w / x ] x = z ) ) |
5 |
1
|
nfsb |
|- F/ y [ w / x ] ph |
6 |
|
equsb3 |
|- ( [ w / x ] x = z <-> w = z ) |
7 |
|
nfv |
|- F/ y w = z |
8 |
6 7
|
nfxfr |
|- F/ y [ w / x ] x = z |
9 |
5 8
|
nfbi |
|- F/ y ( [ w / x ] ph <-> [ w / x ] x = z ) |
10 |
4 9
|
nfxfr |
|- F/ y [ w / x ] ( ph <-> x = z ) |
11 |
|
nfv |
|- F/ w [ y / x ] ( ph <-> x = z ) |
12 |
|
sbequ |
|- ( w = y -> ( [ w / x ] ( ph <-> x = z ) <-> [ y / x ] ( ph <-> x = z ) ) ) |
13 |
10 11 12
|
cbvalv1 |
|- ( A. w [ w / x ] ( ph <-> x = z ) <-> A. y [ y / x ] ( ph <-> x = z ) ) |
14 |
|
equsb3 |
|- ( [ y / x ] x = z <-> y = z ) |
15 |
14
|
sblbis |
|- ( [ y / x ] ( ph <-> x = z ) <-> ( [ y / x ] ph <-> y = z ) ) |
16 |
15
|
albii |
|- ( A. y [ y / x ] ( ph <-> x = z ) <-> A. y ( [ y / x ] ph <-> y = z ) ) |
17 |
3 13 16
|
3bitri |
|- ( A. x ( ph <-> x = z ) <-> A. y ( [ y / x ] ph <-> y = z ) ) |
18 |
17
|
abbii |
|- { z | A. x ( ph <-> x = z ) } = { z | A. y ( [ y / x ] ph <-> y = z ) } |
19 |
18
|
unieqi |
|- U. { z | A. x ( ph <-> x = z ) } = U. { z | A. y ( [ y / x ] ph <-> y = z ) } |
20 |
|
dfiota2 |
|- ( iota x ph ) = U. { z | A. x ( ph <-> x = z ) } |
21 |
|
dfiota2 |
|- ( iota y [ y / x ] ph ) = U. { z | A. y ( [ y / x ] ph <-> y = z ) } |
22 |
19 20 21
|
3eqtr4i |
|- ( iota x ph ) = ( iota y [ y / x ] ph ) |