Step |
Hyp |
Ref |
Expression |
1 |
|
cbviota.1 |
|- ( x = y -> ( ph <-> ps ) ) |
2 |
|
cbviota.2 |
|- F/ y ph |
3 |
|
cbviota.3 |
|- F/ x ps |
4 |
|
nfv |
|- F/ z ( ph <-> x = w ) |
5 |
|
nfs1v |
|- F/ x [ z / x ] ph |
6 |
|
nfv |
|- F/ x z = w |
7 |
5 6
|
nfbi |
|- F/ x ( [ z / x ] ph <-> z = w ) |
8 |
|
sbequ12 |
|- ( x = z -> ( ph <-> [ z / x ] ph ) ) |
9 |
|
equequ1 |
|- ( x = z -> ( x = w <-> z = w ) ) |
10 |
8 9
|
bibi12d |
|- ( x = z -> ( ( ph <-> x = w ) <-> ( [ z / x ] ph <-> z = w ) ) ) |
11 |
4 7 10
|
cbvalv1 |
|- ( A. x ( ph <-> x = w ) <-> A. z ( [ z / x ] ph <-> z = w ) ) |
12 |
2
|
nfsb |
|- F/ y [ z / x ] ph |
13 |
|
nfv |
|- F/ y z = w |
14 |
12 13
|
nfbi |
|- F/ y ( [ z / x ] ph <-> z = w ) |
15 |
|
nfv |
|- F/ z ( ps <-> y = w ) |
16 |
|
sbequ |
|- ( z = y -> ( [ z / x ] ph <-> [ y / x ] ph ) ) |
17 |
3 1
|
sbie |
|- ( [ y / x ] ph <-> ps ) |
18 |
16 17
|
bitrdi |
|- ( z = y -> ( [ z / x ] ph <-> ps ) ) |
19 |
|
equequ1 |
|- ( z = y -> ( z = w <-> y = w ) ) |
20 |
18 19
|
bibi12d |
|- ( z = y -> ( ( [ z / x ] ph <-> z = w ) <-> ( ps <-> y = w ) ) ) |
21 |
14 15 20
|
cbvalv1 |
|- ( A. z ( [ z / x ] ph <-> z = w ) <-> A. y ( ps <-> y = w ) ) |
22 |
11 21
|
bitri |
|- ( A. x ( ph <-> x = w ) <-> A. y ( ps <-> y = w ) ) |
23 |
22
|
abbii |
|- { w | A. x ( ph <-> x = w ) } = { w | A. y ( ps <-> y = w ) } |
24 |
23
|
unieqi |
|- U. { w | A. x ( ph <-> x = w ) } = U. { w | A. y ( ps <-> y = w ) } |
25 |
|
dfiota2 |
|- ( iota x ph ) = U. { w | A. x ( ph <-> x = w ) } |
26 |
|
dfiota2 |
|- ( iota y ps ) = U. { w | A. y ( ps <-> y = w ) } |
27 |
24 25 26
|
3eqtr4i |
|- ( iota x ph ) = ( iota y ps ) |