Step |
Hyp |
Ref |
Expression |
1 |
|
nfe1 |
|- F/ y E. y A. z ( A. y ph -> z = y ) |
2 |
|
nfv |
|- F/ y z e. w |
3 |
|
nfv |
|- F/ y w e. x |
4 |
|
nfa1 |
|- F/ y A. y A. y ph |
5 |
3 4
|
nfan |
|- F/ y ( w e. x /\ A. y A. y ph ) |
6 |
5
|
nfex |
|- F/ y E. w ( w e. x /\ A. y A. y ph ) |
7 |
2 6
|
nfbi |
|- F/ y ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) |
8 |
7
|
nfal |
|- F/ y A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) |
9 |
1 8
|
nfim |
|- F/ y ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) ) |
10 |
9
|
nfex |
|- F/ y E. w ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) ) |
11 |
|
elequ2 |
|- ( y = x -> ( w e. y <-> w e. x ) ) |
12 |
11
|
anbi1d |
|- ( y = x -> ( ( w e. y /\ A. y A. y ph ) <-> ( w e. x /\ A. y A. y ph ) ) ) |
13 |
12
|
exbidv |
|- ( y = x -> ( E. w ( w e. y /\ A. y A. y ph ) <-> E. w ( w e. x /\ A. y A. y ph ) ) ) |
14 |
13
|
bibi2d |
|- ( y = x -> ( ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) <-> ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) ) ) |
15 |
14
|
albidv |
|- ( y = x -> ( A. z ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) <-> A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) ) ) |
16 |
15
|
imbi2d |
|- ( y = x -> ( ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) ) <-> ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) ) ) ) |
17 |
16
|
exbidv |
|- ( y = x -> ( E. w ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) ) <-> E. w ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) ) ) ) |
18 |
|
axrepnd |
|- E. w ( E. y A. z ( A. y ph -> z = y ) -> A. z ( A. y z e. w <-> E. w ( A. z w e. y /\ A. y A. y ph ) ) ) |
19 |
|
19.3v |
|- ( A. y z e. w <-> z e. w ) |
20 |
|
19.3v |
|- ( A. z w e. y <-> w e. y ) |
21 |
20
|
anbi1i |
|- ( ( A. z w e. y /\ A. y A. y ph ) <-> ( w e. y /\ A. y A. y ph ) ) |
22 |
21
|
exbii |
|- ( E. w ( A. z w e. y /\ A. y A. y ph ) <-> E. w ( w e. y /\ A. y A. y ph ) ) |
23 |
19 22
|
bibi12i |
|- ( ( A. y z e. w <-> E. w ( A. z w e. y /\ A. y A. y ph ) ) <-> ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) ) |
24 |
23
|
albii |
|- ( A. z ( A. y z e. w <-> E. w ( A. z w e. y /\ A. y A. y ph ) ) <-> A. z ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) ) |
25 |
24
|
imbi2i |
|- ( ( E. y A. z ( A. y ph -> z = y ) -> A. z ( A. y z e. w <-> E. w ( A. z w e. y /\ A. y A. y ph ) ) ) <-> ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) ) ) |
26 |
25
|
exbii |
|- ( E. w ( E. y A. z ( A. y ph -> z = y ) -> A. z ( A. y z e. w <-> E. w ( A. z w e. y /\ A. y A. y ph ) ) ) <-> E. w ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) ) ) |
27 |
18 26
|
mpbi |
|- E. w ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. y /\ A. y A. y ph ) ) ) |
28 |
10 17 27
|
chvar |
|- E. w ( E. y A. z ( A. y ph -> z = y ) -> A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) ) |
29 |
28
|
19.35i |
|- ( A. w E. y A. z ( A. y ph -> z = y ) -> E. w A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) ) |
30 |
|
nfv |
|- F/ w z e. y |
31 |
|
nfe1 |
|- F/ w E. w ( w e. x /\ A. y ph ) |
32 |
30 31
|
nfbi |
|- F/ w ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) |
33 |
32
|
nfal |
|- F/ w A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) |
34 |
|
elequ2 |
|- ( w = y -> ( z e. w <-> z e. y ) ) |
35 |
|
nfa1 |
|- F/ y A. y ph |
36 |
35
|
19.3 |
|- ( A. y A. y ph <-> A. y ph ) |
37 |
36
|
anbi2i |
|- ( ( w e. x /\ A. y A. y ph ) <-> ( w e. x /\ A. y ph ) ) |
38 |
37
|
exbii |
|- ( E. w ( w e. x /\ A. y A. y ph ) <-> E. w ( w e. x /\ A. y ph ) ) |
39 |
38
|
a1i |
|- ( w = y -> ( E. w ( w e. x /\ A. y A. y ph ) <-> E. w ( w e. x /\ A. y ph ) ) ) |
40 |
34 39
|
bibi12d |
|- ( w = y -> ( ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) <-> ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) ) ) |
41 |
40
|
albidv |
|- ( w = y -> ( A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) <-> A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) ) ) |
42 |
8 33 41
|
cbvexv1 |
|- ( E. w A. z ( z e. w <-> E. w ( w e. x /\ A. y A. y ph ) ) <-> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) ) |
43 |
29 42
|
sylib |
|- ( A. w E. y A. z ( A. y ph -> z = y ) -> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) ) |