Step |
Hyp |
Ref |
Expression |
1 |
|
eu6 |
|- ( E! x ph <-> E. z A. x ( ph <-> x = z ) ) |
2 |
|
sp |
|- ( A. x ( ph <-> x = z ) -> ( ph <-> x = z ) ) |
3 |
|
iotaval |
|- ( A. x ( ph <-> x = z ) -> ( iota x ph ) = z ) |
4 |
3
|
eqeq2d |
|- ( A. x ( ph <-> x = z ) -> ( x = ( iota x ph ) <-> x = z ) ) |
5 |
2 4
|
bitr4d |
|- ( A. x ( ph <-> x = z ) -> ( ph <-> x = ( iota x ph ) ) ) |
6 |
|
eqcom |
|- ( x = ( iota x ph ) <-> ( iota x ph ) = x ) |
7 |
5 6
|
bitrdi |
|- ( A. x ( ph <-> x = z ) -> ( ph <-> ( iota x ph ) = x ) ) |
8 |
7
|
exlimiv |
|- ( E. z A. x ( ph <-> x = z ) -> ( ph <-> ( iota x ph ) = x ) ) |
9 |
1 8
|
sylbi |
|- ( E! x ph -> ( ph <-> ( iota x ph ) = x ) ) |