Description: If a class is not equal to the class in a singleton, then it is not in the singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020) (Proof shortened by BJ, 4-May-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nelsn | |- ( A =/= B -> -. A e. { B } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elsni | |- ( A e. { B } -> A = B ) |
|
| 2 | 1 | necon3ai | |- ( A =/= B -> -. A e. { B } ) |