Step |
Hyp |
Ref |
Expression |
1 |
|
df-ral |
|- ( A. t e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> A. t ( t e. z -> E! v e. z E. u e. y ( z e. u /\ v e. u ) ) ) |
2 |
|
19.23v |
|- ( A. t ( t e. z -> E! v e. z E. u e. y ( z e. u /\ v e. u ) ) <-> ( E. t t e. z -> E! v e. z E. u e. y ( z e. u /\ v e. u ) ) ) |
3 |
1 2
|
bitri |
|- ( A. t e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> ( E. t t e. z -> E! v e. z E. u e. y ( z e. u /\ v e. u ) ) ) |
4 |
|
biidd |
|- ( w = t -> ( E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> E! v e. z E. u e. y ( z e. u /\ v e. u ) ) ) |
5 |
4
|
cbvralvw |
|- ( A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> A. t e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) ) |
6 |
|
n0 |
|- ( z =/= (/) <-> E. t t e. z ) |
7 |
|
elequ2 |
|- ( v = u -> ( z e. v <-> z e. u ) ) |
8 |
|
elequ2 |
|- ( v = u -> ( w e. v <-> w e. u ) ) |
9 |
7 8
|
anbi12d |
|- ( v = u -> ( ( z e. v /\ w e. v ) <-> ( z e. u /\ w e. u ) ) ) |
10 |
9
|
cbvrexvw |
|- ( E. v e. y ( z e. v /\ w e. v ) <-> E. u e. y ( z e. u /\ w e. u ) ) |
11 |
10
|
reubii |
|- ( E! w e. z E. v e. y ( z e. v /\ w e. v ) <-> E! w e. z E. u e. y ( z e. u /\ w e. u ) ) |
12 |
|
elequ1 |
|- ( w = v -> ( w e. u <-> v e. u ) ) |
13 |
12
|
anbi2d |
|- ( w = v -> ( ( z e. u /\ w e. u ) <-> ( z e. u /\ v e. u ) ) ) |
14 |
13
|
rexbidv |
|- ( w = v -> ( E. u e. y ( z e. u /\ w e. u ) <-> E. u e. y ( z e. u /\ v e. u ) ) ) |
15 |
14
|
cbvreuvw |
|- ( E! w e. z E. u e. y ( z e. u /\ w e. u ) <-> E! v e. z E. u e. y ( z e. u /\ v e. u ) ) |
16 |
11 15
|
bitri |
|- ( E! w e. z E. v e. y ( z e. v /\ w e. v ) <-> E! v e. z E. u e. y ( z e. u /\ v e. u ) ) |
17 |
6 16
|
imbi12i |
|- ( ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) <-> ( E. t t e. z -> E! v e. z E. u e. y ( z e. u /\ v e. u ) ) ) |
18 |
3 5 17
|
3bitr4i |
|- ( A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) ) |
19 |
18
|
ralbii |
|- ( A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) ) |
20 |
19
|
exbii |
|- ( E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) ) |