Step |
Hyp |
Ref |
Expression |
1 |
|
df-eu |
|- ( E! x E. y ph <-> ( E. x E. y ph /\ E* x E. y ph ) ) |
2 |
|
excom |
|- ( E. x E. y ph <-> E. y E. x ph ) |
3 |
|
nfe1 |
|- F/ y E. y ph |
4 |
3
|
nfmo |
|- F/ y E* x E. y ph |
5 |
|
19.8a |
|- ( ph -> E. y ph ) |
6 |
5
|
moimi |
|- ( E* x E. y ph -> E* x ph ) |
7 |
|
moeu |
|- ( E* x ph <-> ( E. x ph -> E! x ph ) ) |
8 |
6 7
|
sylib |
|- ( E* x E. y ph -> ( E. x ph -> E! x ph ) ) |
9 |
4 8
|
eximd |
|- ( E* x E. y ph -> ( E. y E. x ph -> E. y E! x ph ) ) |
10 |
2 9
|
syl5bi |
|- ( E* x E. y ph -> ( E. x E. y ph -> E. y E! x ph ) ) |
11 |
10
|
impcom |
|- ( ( E. x E. y ph /\ E* x E. y ph ) -> E. y E! x ph ) |
12 |
1 11
|
sylbi |
|- ( E! x E. y ph -> E. y E! x ph ) |