Step |
Hyp |
Ref |
Expression |
1 |
|
el |
|- E. w x e. w |
2 |
|
nfv |
|- F/ w x e. y |
3 |
|
nfe1 |
|- F/ w E. w ( x e. w /\ w e. y ) |
4 |
2 3
|
nfim |
|- F/ w ( x e. y -> E. w ( x e. w /\ w e. y ) ) |
5 |
4
|
nfal |
|- F/ w A. x ( x e. y -> E. w ( x e. w /\ w e. y ) ) |
6 |
2 5
|
nfan |
|- F/ w ( x e. y /\ A. x ( x e. y -> E. w ( x e. w /\ w e. y ) ) ) |
7 |
6
|
nfex |
|- F/ w E. y ( x e. y /\ A. x ( x e. y -> E. w ( x e. w /\ w e. y ) ) ) |
8 |
|
axinfnd |
|- E. y ( x e. w -> ( x e. y /\ A. x ( x e. y -> E. w ( x e. w /\ w e. y ) ) ) ) |
9 |
8
|
19.37iv |
|- ( x e. w -> E. y ( x e. y /\ A. x ( x e. y -> E. w ( x e. w /\ w e. y ) ) ) ) |
10 |
7 9
|
exlimi |
|- ( E. w x e. w -> E. y ( x e. y /\ A. x ( x e. y -> E. w ( x e. w /\ w e. y ) ) ) ) |
11 |
1 10
|
ax-mp |
|- E. y ( x e. y /\ A. x ( x e. y -> E. w ( x e. w /\ w e. y ) ) ) |
12 |
|
elequ1 |
|- ( z = x -> ( z e. y <-> x e. y ) ) |
13 |
|
elequ1 |
|- ( z = x -> ( z e. w <-> x e. w ) ) |
14 |
13
|
anbi1d |
|- ( z = x -> ( ( z e. w /\ w e. y ) <-> ( x e. w /\ w e. y ) ) ) |
15 |
14
|
exbidv |
|- ( z = x -> ( E. w ( z e. w /\ w e. y ) <-> E. w ( x e. w /\ w e. y ) ) ) |
16 |
12 15
|
imbi12d |
|- ( z = x -> ( ( z e. y -> E. w ( z e. w /\ w e. y ) ) <-> ( x e. y -> E. w ( x e. w /\ w e. y ) ) ) ) |
17 |
16
|
cbvalvw |
|- ( A. z ( z e. y -> E. w ( z e. w /\ w e. y ) ) <-> A. x ( x e. y -> E. w ( x e. w /\ w e. y ) ) ) |
18 |
17
|
anbi2i |
|- ( ( x e. y /\ A. z ( z e. y -> E. w ( z e. w /\ w e. y ) ) ) <-> ( x e. y /\ A. x ( x e. y -> E. w ( x e. w /\ w e. y ) ) ) ) |
19 |
18
|
exbii |
|- ( E. y ( x e. y /\ A. z ( z e. y -> E. w ( z e. w /\ w e. y ) ) ) <-> E. y ( x e. y /\ A. x ( x e. y -> E. w ( x e. w /\ w e. y ) ) ) ) |
20 |
11 19
|
mpbir |
|- E. y ( x e. y /\ A. z ( z e. y -> E. w ( z e. w /\ w e. y ) ) ) |