Step |
Hyp |
Ref |
Expression |
1 |
|
ralnex |
|- ( A. z e. u -. A. w e. z ps <-> -. E. z e. u A. w e. z ps ) |
2 |
|
df-rex |
|- ( E. w e. z -. ps <-> E. w ( w e. z /\ -. ps ) ) |
3 |
|
rexnal |
|- ( E. w e. z -. ps <-> -. A. w e. z ps ) |
4 |
2 3
|
bitr3i |
|- ( E. w ( w e. z /\ -. ps ) <-> -. A. w e. z ps ) |
5 |
|
exsimpl |
|- ( E. w ( w e. z /\ -. ps ) -> E. w w e. z ) |
6 |
|
n0 |
|- ( z =/= (/) <-> E. w w e. z ) |
7 |
5 6
|
sylibr |
|- ( E. w ( w e. z /\ -. ps ) -> z =/= (/) ) |
8 |
4 7
|
sylbir |
|- ( -. A. w e. z ps -> z =/= (/) ) |
9 |
8
|
ralimi |
|- ( A. z e. u -. A. w e. z ps -> A. z e. u z =/= (/) ) |
10 |
1 9
|
sylbir |
|- ( -. E. z e. u A. w e. z ps -> A. z e. u z =/= (/) ) |
11 |
|
kmlem2 |
|- ( E. y A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) <-> E. y ( -. y e. u /\ A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) ) |
12 |
|
biimt |
|- ( z =/= (/) -> ( E! w w e. ( z i^i y ) <-> ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) ) |
13 |
12
|
ralimi |
|- ( A. z e. u z =/= (/) -> A. z e. u ( E! w w e. ( z i^i y ) <-> ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) ) |
14 |
|
ralbi |
|- ( A. z e. u ( E! w w e. ( z i^i y ) <-> ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) -> ( A. z e. u E! w w e. ( z i^i y ) <-> A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) ) |
15 |
13 14
|
syl |
|- ( A. z e. u z =/= (/) -> ( A. z e. u E! w w e. ( z i^i y ) <-> A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) ) |
16 |
15
|
anbi2d |
|- ( A. z e. u z =/= (/) -> ( ( -. y e. u /\ A. z e. u E! w w e. ( z i^i y ) ) <-> ( -. y e. u /\ A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) ) ) |
17 |
16
|
exbidv |
|- ( A. z e. u z =/= (/) -> ( E. y ( -. y e. u /\ A. z e. u E! w w e. ( z i^i y ) ) <-> E. y ( -. y e. u /\ A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) ) ) |
18 |
11 17
|
bitr4id |
|- ( A. z e. u z =/= (/) -> ( E. y A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) <-> E. y ( -. y e. u /\ A. z e. u E! w w e. ( z i^i y ) ) ) ) |
19 |
10 18
|
syl |
|- ( -. E. z e. u A. w e. z ps -> ( E. y A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) <-> E. y ( -. y e. u /\ A. z e. u E! w w e. ( z i^i y ) ) ) ) |
20 |
19
|
pm5.74i |
|- ( ( -. E. z e. u A. w e. z ps -> E. y A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) <-> ( -. E. z e. u A. w e. z ps -> E. y ( -. y e. u /\ A. z e. u E! w w e. ( z i^i y ) ) ) ) |
21 |
|
pm4.64 |
|- ( ( -. E. z e. u A. w e. z ps -> E. y ( -. y e. u /\ A. z e. u E! w w e. ( z i^i y ) ) ) <-> ( E. z e. u A. w e. z ps \/ E. y ( -. y e. u /\ A. z e. u E! w w e. ( z i^i y ) ) ) ) |
22 |
20 21
|
bitri |
|- ( ( -. E. z e. u A. w e. z ps -> E. y A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) <-> ( E. z e. u A. w e. z ps \/ E. y ( -. y e. u /\ A. z e. u E! w w e. ( z i^i y ) ) ) ) |