Step |
Hyp |
Ref |
Expression |
1 |
|
axrep4.1 |
|- F/ z ph |
2 |
|
axrep3 |
|- E. x ( E. z A. y ( ph -> y = z ) -> A. y ( y e. x <-> E. x ( x e. w /\ A. z ph ) ) ) |
3 |
2
|
19.35i |
|- ( A. x E. z A. y ( ph -> y = z ) -> E. x A. y ( y e. x <-> E. x ( x e. w /\ A. z ph ) ) ) |
4 |
|
nfv |
|- F/ z y e. x |
5 |
|
nfv |
|- F/ z x e. w |
6 |
|
nfa1 |
|- F/ z A. z ph |
7 |
5 6
|
nfan |
|- F/ z ( x e. w /\ A. z ph ) |
8 |
7
|
nfex |
|- F/ z E. x ( x e. w /\ A. z ph ) |
9 |
4 8
|
nfbi |
|- F/ z ( y e. x <-> E. x ( x e. w /\ A. z ph ) ) |
10 |
9
|
nfal |
|- F/ z A. y ( y e. x <-> E. x ( x e. w /\ A. z ph ) ) |
11 |
|
nfv |
|- F/ x y e. z |
12 |
|
nfe1 |
|- F/ x E. x ( x e. w /\ ph ) |
13 |
11 12
|
nfbi |
|- F/ x ( y e. z <-> E. x ( x e. w /\ ph ) ) |
14 |
13
|
nfal |
|- F/ x A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) |
15 |
|
elequ2 |
|- ( x = z -> ( y e. x <-> y e. z ) ) |
16 |
1
|
19.3 |
|- ( A. z ph <-> ph ) |
17 |
16
|
anbi2i |
|- ( ( x e. w /\ A. z ph ) <-> ( x e. w /\ ph ) ) |
18 |
17
|
exbii |
|- ( E. x ( x e. w /\ A. z ph ) <-> E. x ( x e. w /\ ph ) ) |
19 |
18
|
a1i |
|- ( x = z -> ( E. x ( x e. w /\ A. z ph ) <-> E. x ( x e. w /\ ph ) ) ) |
20 |
15 19
|
bibi12d |
|- ( x = z -> ( ( y e. x <-> E. x ( x e. w /\ A. z ph ) ) <-> ( y e. z <-> E. x ( x e. w /\ ph ) ) ) ) |
21 |
20
|
albidv |
|- ( x = z -> ( A. y ( y e. x <-> E. x ( x e. w /\ A. z ph ) ) <-> A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) ) ) |
22 |
10 14 21
|
cbvexv1 |
|- ( E. x A. y ( y e. x <-> E. x ( x e. w /\ A. z ph ) ) <-> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) ) |
23 |
3 22
|
sylib |
|- ( A. x E. z A. y ( ph -> y = z ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) ) |