Step |
Hyp |
Ref |
Expression |
1 |
|
vsnid |
|- x e. { x } |
2 |
|
snex |
|- { x } e. _V |
3 |
|
eleq2 |
|- ( z = { x } -> ( x e. z <-> x e. { x } ) ) |
4 |
|
eleq2 |
|- ( z = { x } -> ( y e. z <-> y e. { x } ) ) |
5 |
3 4
|
imbi12d |
|- ( z = { x } -> ( ( x e. z -> y e. z ) <-> ( x e. { x } -> y e. { x } ) ) ) |
6 |
2 5
|
spcv |
|- ( A. z ( x e. z -> y e. z ) -> ( x e. { x } -> y e. { x } ) ) |
7 |
1 6
|
mpi |
|- ( A. z ( x e. z -> y e. z ) -> y e. { x } ) |
8 |
|
velsn |
|- ( y e. { x } <-> y = x ) |
9 |
|
equcomi |
|- ( y = x -> x = y ) |
10 |
8 9
|
sylbi |
|- ( y e. { x } -> x = y ) |
11 |
7 10
|
syl |
|- ( A. z ( x e. z -> y e. z ) -> x = y ) |