Description: A singleton is a set. See also snex , snexALT . (Contributed by NM, 7-Aug-1994) Prove it from ax-bj-sn . (Revised by BJ, 12-Jan-2025) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-snex | |- { A } e. _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-snexg | |- ( A e. _V -> { A } e. _V ) |
|
| 2 | snprc | |- ( -. A e. _V <-> { A } = (/) ) |
|
| 3 | 2 | biimpi | |- ( -. A e. _V -> { A } = (/) ) |
| 4 | 0ex | |- (/) e. _V |
|
| 5 | 3 4 | eqeltrdi | |- ( -. A e. _V -> { A } e. _V ) |
| 6 | 1 5 | pm2.61i | |- { A } e. _V |