Step |
Hyp |
Ref |
Expression |
1 |
|
df-ne |
|- ( A =/= (/) <-> -. A = (/) ) |
2 |
|
biorf |
|- ( -. A = (/) -> ( A = { B } <-> ( A = (/) \/ A = { B } ) ) ) |
3 |
1 2
|
sylbi |
|- ( A =/= (/) -> ( A = { B } <-> ( A = (/) \/ A = { B } ) ) ) |
4 |
|
dfss3 |
|- ( A C_ { B } <-> A. x e. A x e. { B } ) |
5 |
|
sssn |
|- ( A C_ { B } <-> ( A = (/) \/ A = { B } ) ) |
6 |
|
velsn |
|- ( x e. { B } <-> x = B ) |
7 |
6
|
ralbii |
|- ( A. x e. A x e. { B } <-> A. x e. A x = B ) |
8 |
4 5 7
|
3bitr3i |
|- ( ( A = (/) \/ A = { B } ) <-> A. x e. A x = B ) |
9 |
3 8
|
bitrdi |
|- ( A =/= (/) -> ( A = { B } <-> A. x e. A x = B ) ) |