Step |
Hyp |
Ref |
Expression |
1 |
|
sb8v |
|- ( A. x ( x e. A -> ph ) <-> A. y [ y / x ] ( x e. A -> ph ) ) |
2 |
|
df-ral |
|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) ) |
3 |
|
df-ral |
|- ( A. y e. A [ y / x ] ph <-> A. y ( y e. A -> [ y / x ] ph ) ) |
4 |
|
eleq1w |
|- ( x = y -> ( x e. A <-> y e. A ) ) |
5 |
4
|
imbi1d |
|- ( x = y -> ( ( x e. A -> ph ) <-> ( y e. A -> ph ) ) ) |
6 |
5
|
pm5.74i |
|- ( ( x = y -> ( x e. A -> ph ) ) <-> ( x = y -> ( y e. A -> ph ) ) ) |
7 |
6
|
albii |
|- ( A. x ( x = y -> ( x e. A -> ph ) ) <-> A. x ( x = y -> ( y e. A -> ph ) ) ) |
8 |
|
sb6 |
|- ( [ y / x ] ( x e. A -> ph ) <-> A. x ( x = y -> ( x e. A -> ph ) ) ) |
9 |
|
sb6 |
|- ( [ y / x ] ( y e. A -> ph ) <-> A. x ( x = y -> ( y e. A -> ph ) ) ) |
10 |
7 8 9
|
3bitr4i |
|- ( [ y / x ] ( x e. A -> ph ) <-> [ y / x ] ( y e. A -> ph ) ) |
11 |
|
sbrimvw |
|- ( [ y / x ] ( y e. A -> ph ) <-> ( y e. A -> [ y / x ] ph ) ) |
12 |
10 11
|
bitr2i |
|- ( ( y e. A -> [ y / x ] ph ) <-> [ y / x ] ( x e. A -> ph ) ) |
13 |
12
|
albii |
|- ( A. y ( y e. A -> [ y / x ] ph ) <-> A. y [ y / x ] ( x e. A -> ph ) ) |
14 |
3 13
|
bitri |
|- ( A. y e. A [ y / x ] ph <-> A. y [ y / x ] ( x e. A -> ph ) ) |
15 |
1 2 14
|
3bitr4i |
|- ( A. x e. A ph <-> A. y e. A [ y / x ] ph ) |