Step |
Hyp |
Ref |
Expression |
1 |
|
sb8f.nf |
|- F/ y ph |
2 |
|
sb6 |
|- ( [ y / x ] ph <-> A. x ( x = y -> ph ) ) |
3 |
2
|
albii |
|- ( A. y [ y / x ] ph <-> A. y A. x ( x = y -> ph ) ) |
4 |
|
alcom |
|- ( A. y A. x ( x = y -> ph ) <-> A. x A. y ( x = y -> ph ) ) |
5 |
|
sb6 |
|- ( [ x / y ] ph <-> A. y ( y = x -> ph ) ) |
6 |
1
|
sbf |
|- ( [ x / y ] ph <-> ph ) |
7 |
|
equcom |
|- ( y = x <-> x = y ) |
8 |
7
|
imbi1i |
|- ( ( y = x -> ph ) <-> ( x = y -> ph ) ) |
9 |
8
|
albii |
|- ( A. y ( y = x -> ph ) <-> A. y ( x = y -> ph ) ) |
10 |
5 6 9
|
3bitr3ri |
|- ( A. y ( x = y -> ph ) <-> ph ) |
11 |
10
|
albii |
|- ( A. x A. y ( x = y -> ph ) <-> A. x ph ) |
12 |
3 4 11
|
3bitrri |
|- ( A. x ph <-> A. y [ y / x ] ph ) |