Step |
Hyp |
Ref |
Expression |
1 |
|
en1 |
|- ( B ~~ 1o <-> E. x B = { x } ) |
2 |
|
eleq2 |
|- ( B = { x } -> ( A e. B <-> A e. { x } ) ) |
3 |
|
elsni |
|- ( A e. { x } -> A = x ) |
4 |
3
|
sneqd |
|- ( A e. { x } -> { A } = { x } ) |
5 |
2 4
|
syl6bi |
|- ( B = { x } -> ( A e. B -> { A } = { x } ) ) |
6 |
5
|
imp |
|- ( ( B = { x } /\ A e. B ) -> { A } = { x } ) |
7 |
|
eqtr3 |
|- ( ( B = { x } /\ { A } = { x } ) -> B = { A } ) |
8 |
6 7
|
syldan |
|- ( ( B = { x } /\ A e. B ) -> B = { A } ) |
9 |
8
|
ex |
|- ( B = { x } -> ( A e. B -> B = { A } ) ) |
10 |
9
|
exlimiv |
|- ( E. x B = { x } -> ( A e. B -> B = { A } ) ) |
11 |
1 10
|
sylbi |
|- ( B ~~ 1o -> ( A e. B -> B = { A } ) ) |
12 |
11
|
impcom |
|- ( ( A e. B /\ B ~~ 1o ) -> B = { A } ) |