Step |
Hyp |
Ref |
Expression |
1 |
|
bj-cbvaldv.1 |
|- F/ y ph |
2 |
|
bj-cbvaldv.2 |
|- ( ph -> F/ y ps ) |
3 |
|
bj-cbvaldv.3 |
|- ( ph -> ( x = y -> ( ps <-> ch ) ) ) |
4 |
2
|
nfnd |
|- ( ph -> F/ y -. ps ) |
5 |
|
notbi |
|- ( ( ps <-> ch ) <-> ( -. ps <-> -. ch ) ) |
6 |
3 5
|
syl6ib |
|- ( ph -> ( x = y -> ( -. ps <-> -. ch ) ) ) |
7 |
1 4 6
|
bj-cbvaldv |
|- ( ph -> ( A. x -. ps <-> A. y -. ch ) ) |
8 |
7
|
notbid |
|- ( ph -> ( -. A. x -. ps <-> -. A. y -. ch ) ) |
9 |
|
df-ex |
|- ( E. x ps <-> -. A. x -. ps ) |
10 |
|
df-ex |
|- ( E. y ch <-> -. A. y -. ch ) |
11 |
8 9 10
|
3bitr4g |
|- ( ph -> ( E. x ps <-> E. y ch ) ) |