| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ax-sep |
|- E. z A. x ( x e. z <-> ( x e. y /\ ph ) ) |
| 2 |
|
bimsc1 |
|- ( ( ( ph -> x e. y ) /\ ( x e. z <-> ( x e. y /\ ph ) ) ) -> ( x e. z <-> ph ) ) |
| 3 |
2
|
ex |
|- ( ( ph -> x e. y ) -> ( ( x e. z <-> ( x e. y /\ ph ) ) -> ( x e. z <-> ph ) ) ) |
| 4 |
3
|
al2imi |
|- ( A. x ( ph -> x e. y ) -> ( A. x ( x e. z <-> ( x e. y /\ ph ) ) -> A. x ( x e. z <-> ph ) ) ) |
| 5 |
4
|
eximdv |
|- ( A. x ( ph -> x e. y ) -> ( E. z A. x ( x e. z <-> ( x e. y /\ ph ) ) -> E. z A. x ( x e. z <-> ph ) ) ) |
| 6 |
1 5
|
mpi |
|- ( A. x ( ph -> x e. y ) -> E. z A. x ( x e. z <-> ph ) ) |
| 7 |
6
|
exlimiv |
|- ( E. y A. x ( ph -> x e. y ) -> E. z A. x ( x e. z <-> ph ) ) |