Step |
Hyp |
Ref |
Expression |
1 |
|
alexn |
|- ( A. x E. y -. y e. x <-> -. E. x A. y y e. x ) |
2 |
|
ax-sep |
|- E. y A. z ( z e. y <-> ( z e. x /\ -. z e. z ) ) |
3 |
|
elequ1 |
|- ( z = y -> ( z e. y <-> y e. y ) ) |
4 |
|
elequ1 |
|- ( z = y -> ( z e. x <-> y e. x ) ) |
5 |
|
elequ1 |
|- ( z = y -> ( z e. z <-> y e. z ) ) |
6 |
|
elequ2 |
|- ( z = y -> ( y e. z <-> y e. y ) ) |
7 |
5 6
|
bitrd |
|- ( z = y -> ( z e. z <-> y e. y ) ) |
8 |
7
|
notbid |
|- ( z = y -> ( -. z e. z <-> -. y e. y ) ) |
9 |
4 8
|
anbi12d |
|- ( z = y -> ( ( z e. x /\ -. z e. z ) <-> ( y e. x /\ -. y e. y ) ) ) |
10 |
3 9
|
bibi12d |
|- ( z = y -> ( ( z e. y <-> ( z e. x /\ -. z e. z ) ) <-> ( y e. y <-> ( y e. x /\ -. y e. y ) ) ) ) |
11 |
10
|
spvv |
|- ( A. z ( z e. y <-> ( z e. x /\ -. z e. z ) ) -> ( y e. y <-> ( y e. x /\ -. y e. y ) ) ) |
12 |
|
pclem6 |
|- ( ( y e. y <-> ( y e. x /\ -. y e. y ) ) -> -. y e. x ) |
13 |
11 12
|
syl |
|- ( A. z ( z e. y <-> ( z e. x /\ -. z e. z ) ) -> -. y e. x ) |
14 |
2 13
|
eximii |
|- E. y -. y e. x |
15 |
1 14
|
mpgbi |
|- -. E. x A. y y e. x |