Step |
Hyp |
Ref |
Expression |
1 |
|
reu8nf.1 |
|- F/ x ps |
2 |
|
reu8nf.2 |
|- F/ x ch |
3 |
|
reu8nf.3 |
|- ( x = w -> ( ph <-> ch ) ) |
4 |
|
reu8nf.4 |
|- ( w = y -> ( ch <-> ps ) ) |
5 |
|
nfv |
|- F/ w ph |
6 |
5 2 3
|
cbvreuw |
|- ( E! x e. A ph <-> E! w e. A ch ) |
7 |
4
|
reu8 |
|- ( E! w e. A ch <-> E. w e. A ( ch /\ A. y e. A ( ps -> w = y ) ) ) |
8 |
|
nfcv |
|- F/_ x A |
9 |
|
nfv |
|- F/ x w = y |
10 |
1 9
|
nfim |
|- F/ x ( ps -> w = y ) |
11 |
8 10
|
nfralw |
|- F/ x A. y e. A ( ps -> w = y ) |
12 |
2 11
|
nfan |
|- F/ x ( ch /\ A. y e. A ( ps -> w = y ) ) |
13 |
|
nfv |
|- F/ w ( ph /\ A. y e. A ( ps -> x = y ) ) |
14 |
3
|
bicomd |
|- ( x = w -> ( ch <-> ph ) ) |
15 |
14
|
equcoms |
|- ( w = x -> ( ch <-> ph ) ) |
16 |
|
equequ1 |
|- ( w = x -> ( w = y <-> x = y ) ) |
17 |
16
|
imbi2d |
|- ( w = x -> ( ( ps -> w = y ) <-> ( ps -> x = y ) ) ) |
18 |
17
|
ralbidv |
|- ( w = x -> ( A. y e. A ( ps -> w = y ) <-> A. y e. A ( ps -> x = y ) ) ) |
19 |
15 18
|
anbi12d |
|- ( w = x -> ( ( ch /\ A. y e. A ( ps -> w = y ) ) <-> ( ph /\ A. y e. A ( ps -> x = y ) ) ) ) |
20 |
12 13 19
|
cbvrexw |
|- ( E. w e. A ( ch /\ A. y e. A ( ps -> w = y ) ) <-> E. x e. A ( ph /\ A. y e. A ( ps -> x = y ) ) ) |
21 |
6 7 20
|
3bitri |
|- ( E! x e. A ph <-> E. x e. A ( ph /\ A. y e. A ( ps -> x = y ) ) ) |