Step |
Hyp |
Ref |
Expression |
1 |
|
el |
|- E. z x e. z |
2 |
|
df-ex |
|- ( E. z x e. z <-> -. A. z -. x e. z ) |
3 |
|
nfnae |
|- F/ y -. A. y y = x |
4 |
|
dveel1 |
|- ( -. A. y y = x -> ( x e. z -> A. y x e. z ) ) |
5 |
3 4
|
nf5d |
|- ( -. A. y y = x -> F/ y x e. z ) |
6 |
5
|
nfnd |
|- ( -. A. y y = x -> F/ y -. x e. z ) |
7 |
|
elequ2 |
|- ( z = y -> ( x e. z <-> x e. y ) ) |
8 |
7
|
notbid |
|- ( z = y -> ( -. x e. z <-> -. x e. y ) ) |
9 |
8
|
a1i |
|- ( -. A. y y = x -> ( z = y -> ( -. x e. z <-> -. x e. y ) ) ) |
10 |
3 6 9
|
cbvald |
|- ( -. A. y y = x -> ( A. z -. x e. z <-> A. y -. x e. y ) ) |
11 |
10
|
notbid |
|- ( -. A. y y = x -> ( -. A. z -. x e. z <-> -. A. y -. x e. y ) ) |
12 |
2 11
|
syl5bb |
|- ( -. A. y y = x -> ( E. z x e. z <-> -. A. y -. x e. y ) ) |
13 |
1 12
|
mpbii |
|- ( -. A. y y = x -> -. A. y -. x e. y ) |
14 |
|
elirrv |
|- -. y e. y |
15 |
|
elequ1 |
|- ( y = x -> ( y e. y <-> x e. y ) ) |
16 |
14 15
|
mtbii |
|- ( y = x -> -. x e. y ) |
17 |
16
|
alimi |
|- ( A. y y = x -> A. y -. x e. y ) |
18 |
17
|
con3i |
|- ( -. A. y -. x e. y -> -. A. y y = x ) |
19 |
13 18
|
impbii |
|- ( -. A. y y = x <-> -. A. y -. x e. y ) |