Description: If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | sneqr.1 | |- A e. _V |
|
| Assertion | snsssn | |- ( { A } C_ { B } -> A = B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sneqr.1 | |- A e. _V |
|
| 2 | sssn | |- ( { A } C_ { B } <-> ( { A } = (/) \/ { A } = { B } ) ) |
|
| 3 | 1 | snnz | |- { A } =/= (/) |
| 4 | 3 | neii | |- -. { A } = (/) |
| 5 | 4 | pm2.21i | |- ( { A } = (/) -> A = B ) |
| 6 | 1 | sneqr | |- ( { A } = { B } -> A = B ) |
| 7 | 5 6 | jaoi | |- ( ( { A } = (/) \/ { A } = { B } ) -> A = B ) |
| 8 | 2 7 | sylbi | |- ( { A } C_ { B } -> A = B ) |