Step |
Hyp |
Ref |
Expression |
1 |
|
cbvmowOLD.1 |
|- F/ y ph |
2 |
|
cbvmowOLD.2 |
|- F/ x ps |
3 |
|
cbvmowOLD.3 |
|- ( x = y -> ( ph <-> ps ) ) |
4 |
1
|
sb8ev |
|- ( E. x ph <-> E. y [ y / x ] ph ) |
5 |
1
|
sb8euv |
|- ( E! x ph <-> E! y [ y / x ] ph ) |
6 |
4 5
|
imbi12i |
|- ( ( E. x ph -> E! x ph ) <-> ( E. y [ y / x ] ph -> E! y [ y / x ] ph ) ) |
7 |
|
moeu |
|- ( E* x ph <-> ( E. x ph -> E! x ph ) ) |
8 |
|
moeu |
|- ( E* y [ y / x ] ph <-> ( E. y [ y / x ] ph -> E! y [ y / x ] ph ) ) |
9 |
6 7 8
|
3bitr4i |
|- ( E* x ph <-> E* y [ y / x ] ph ) |
10 |
2 3
|
sbiev |
|- ( [ y / x ] ph <-> ps ) |
11 |
10
|
mobii |
|- ( E* y [ y / x ] ph <-> E* y ps ) |
12 |
9 11
|
bitri |
|- ( E* x ph <-> E* y ps ) |