Step |
Hyp |
Ref |
Expression |
1 |
|
nfe1 |
|- F/ y E. y A. z ( ph -> z = y ) |
2 |
|
nfv |
|- F/ y z e. x |
3 |
|
nfv |
|- F/ y x e. w |
4 |
|
nfa1 |
|- F/ y A. y ph |
5 |
3 4
|
nfan |
|- F/ y ( x e. w /\ A. y ph ) |
6 |
5
|
nfex |
|- F/ y E. x ( x e. w /\ A. y ph ) |
7 |
2 6
|
nfbi |
|- F/ y ( z e. x <-> E. x ( x e. w /\ A. y ph ) ) |
8 |
7
|
nfal |
|- F/ y A. z ( z e. x <-> E. x ( x e. w /\ A. y ph ) ) |
9 |
1 8
|
nfim |
|- F/ y ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. w /\ A. y ph ) ) ) |
10 |
9
|
nfex |
|- F/ y E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. w /\ A. y ph ) ) ) |
11 |
|
axreplem |
|- ( y = w -> ( E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) <-> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. w /\ A. y ph ) ) ) ) ) |
12 |
|
axrep2 |
|- E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) |
13 |
10 11 12
|
chvarfv |
|- E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. w /\ A. y ph ) ) ) |