Step |
Hyp |
Ref |
Expression |
1 |
|
eqeq2 |
|- ( y = A -> ( x = y <-> x = A ) ) |
2 |
1
|
imbi2d |
|- ( y = A -> ( ( ph -> x = y ) <-> ( ph -> x = A ) ) ) |
3 |
2
|
albidv |
|- ( y = A -> ( A. x ( ph -> x = y ) <-> A. x ( ph -> x = A ) ) ) |
4 |
3
|
imbi1d |
|- ( y = A -> ( ( A. x ( ph -> x = y ) -> E* x ph ) <-> ( A. x ( ph -> x = A ) -> E* x ph ) ) ) |
5 |
|
19.8a |
|- ( A. x ( ph -> x = y ) -> E. y A. x ( ph -> x = y ) ) |
6 |
|
df-mo |
|- ( E* x ph <-> E. y A. x ( ph -> x = y ) ) |
7 |
5 6
|
sylibr |
|- ( A. x ( ph -> x = y ) -> E* x ph ) |
8 |
4 7
|
vtoclg |
|- ( A e. _V -> ( A. x ( ph -> x = A ) -> E* x ph ) ) |
9 |
|
eqvisset |
|- ( x = A -> A e. _V ) |
10 |
9
|
imim2i |
|- ( ( ph -> x = A ) -> ( ph -> A e. _V ) ) |
11 |
10
|
con3rr3 |
|- ( -. A e. _V -> ( ( ph -> x = A ) -> -. ph ) ) |
12 |
11
|
alimdv |
|- ( -. A e. _V -> ( A. x ( ph -> x = A ) -> A. x -. ph ) ) |
13 |
|
alnex |
|- ( A. x -. ph <-> -. E. x ph ) |
14 |
|
nexmo |
|- ( -. E. x ph -> E* x ph ) |
15 |
13 14
|
sylbi |
|- ( A. x -. ph -> E* x ph ) |
16 |
12 15
|
syl6 |
|- ( -. A e. _V -> ( A. x ( ph -> x = A ) -> E* x ph ) ) |
17 |
8 16
|
pm2.61i |
|- ( A. x ( ph -> x = A ) -> E* x ph ) |