Step |
Hyp |
Ref |
Expression |
1 |
|
equequ2 |
|- ( z = y -> ( x = z <-> x = y ) ) |
2 |
1
|
bibi2d |
|- ( z = y -> ( ( { x } = { y } <-> x = z ) <-> ( { x } = { y } <-> x = y ) ) ) |
3 |
2
|
albidv |
|- ( z = y -> ( A. x ( { x } = { y } <-> x = z ) <-> A. x ( { x } = { y } <-> x = y ) ) ) |
4 |
|
sneqbg |
|- ( x e. _V -> ( { x } = { y } <-> x = y ) ) |
5 |
4
|
elv |
|- ( { x } = { y } <-> x = y ) |
6 |
5
|
ax-gen |
|- A. x ( { x } = { y } <-> x = y ) |
7 |
3 6
|
speivw |
|- E. z A. x ( { x } = { y } <-> x = z ) |
8 |
|
eu6 |
|- ( E! x { x } = { y } <-> E. z A. x ( { x } = { y } <-> x = z ) ) |
9 |
7 8
|
mpbir |
|- E! x { x } = { y } |