Step |
Hyp |
Ref |
Expression |
1 |
|
dfmoeu |
|- ( ( E. x ph -> E. y A. x ( ph <-> x = y ) ) <-> E. y A. x ( ph -> x = y ) ) |
2 |
1
|
anbi2i |
|- ( ( E. x ph /\ ( E. x ph -> E. y A. x ( ph <-> x = y ) ) ) <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) ) |
3 |
|
abai |
|- ( ( E. x ph /\ E. y A. x ( ph <-> x = y ) ) <-> ( E. x ph /\ ( E. x ph -> E. y A. x ( ph <-> x = y ) ) ) ) |
4 |
|
eu3v |
|- ( E! x ph <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) ) |
5 |
2 3 4
|
3bitr4ri |
|- ( E! x ph <-> ( E. x ph /\ E. y A. x ( ph <-> x = y ) ) ) |
6 |
|
abai |
|- ( ( E. y A. x ( ph <-> x = y ) /\ E. x ph ) <-> ( E. y A. x ( ph <-> x = y ) /\ ( E. y A. x ( ph <-> x = y ) -> E. x ph ) ) ) |
7 |
|
ancom |
|- ( ( E. x ph /\ E. y A. x ( ph <-> x = y ) ) <-> ( E. y A. x ( ph <-> x = y ) /\ E. x ph ) ) |
8 |
|
biimpr |
|- ( ( ph <-> x = y ) -> ( x = y -> ph ) ) |
9 |
8
|
alimi |
|- ( A. x ( ph <-> x = y ) -> A. x ( x = y -> ph ) ) |
10 |
9
|
eximi |
|- ( E. y A. x ( ph <-> x = y ) -> E. y A. x ( x = y -> ph ) ) |
11 |
|
exsbim |
|- ( E. y A. x ( x = y -> ph ) -> E. x ph ) |
12 |
10 11
|
syl |
|- ( E. y A. x ( ph <-> x = y ) -> E. x ph ) |
13 |
12
|
biantru |
|- ( E. y A. x ( ph <-> x = y ) <-> ( E. y A. x ( ph <-> x = y ) /\ ( E. y A. x ( ph <-> x = y ) -> E. x ph ) ) ) |
14 |
6 7 13
|
3bitr4i |
|- ( ( E. x ph /\ E. y A. x ( ph <-> x = y ) ) <-> E. y A. x ( ph <-> x = y ) ) |
15 |
5 14
|
bitri |
|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) ) |