Step |
Hyp |
Ref |
Expression |
1 |
|
exel |
|- E. x E. z z e. x |
2 |
|
ax-nul |
|- E. y A. z -. z e. y |
3 |
|
exdistrv |
|- ( E. x E. y ( E. z z e. x /\ A. z -. z e. y ) <-> ( E. x E. z z e. x /\ E. y A. z -. z e. y ) ) |
4 |
1 2 3
|
mpbir2an |
|- E. x E. y ( E. z z e. x /\ A. z -. z e. y ) |
5 |
|
ax9v1 |
|- ( x = y -> ( z e. x -> z e. y ) ) |
6 |
5
|
eximdv |
|- ( x = y -> ( E. z z e. x -> E. z z e. y ) ) |
7 |
|
df-ex |
|- ( E. z z e. y <-> -. A. z -. z e. y ) |
8 |
6 7
|
imbitrdi |
|- ( x = y -> ( E. z z e. x -> -. A. z -. z e. y ) ) |
9 |
8
|
com12 |
|- ( E. z z e. x -> ( x = y -> -. A. z -. z e. y ) ) |
10 |
9
|
con2d |
|- ( E. z z e. x -> ( A. z -. z e. y -> -. x = y ) ) |
11 |
10
|
imp |
|- ( ( E. z z e. x /\ A. z -. z e. y ) -> -. x = y ) |
12 |
11
|
2eximi |
|- ( E. x E. y ( E. z z e. x /\ A. z -. z e. y ) -> E. x E. y -. x = y ) |
13 |
4 12
|
ax-mp |
|- E. x E. y -. x = y |