Description: If the singletons of two sets are equal, the two sets are equal. Part of Exercise 4 of TakeutiZaring p. 15. (Contributed by NM, 27-Aug-1993)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | sneqr.1 | |- A e. _V |
|
| Assertion | sneqr | |- ( { A } = { B } -> A = B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sneqr.1 | |- A e. _V |
|
| 2 | sneqrg | |- ( A e. _V -> ( { A } = { B } -> A = B ) ) |
|
| 3 | 1 2 | ax-mp | |- ( { A } = { B } -> A = B ) |