Description: A singleton is a Moore collection, biconditional version. (Contributed by BJ, 9-Dec-2021) (Proof shortened by BJ, 10-Apr-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-snmooreb | |- ( A e. _V <-> { A } e. Moore_ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-snmoore | |- ( A e. _V -> { A } e. Moore_ ) |
|
| 2 | snprc | |- ( -. A e. _V <-> { A } = (/) ) |
|
| 3 | 2 | biimpi | |- ( -. A e. _V -> { A } = (/) ) |
| 4 | bj-0nmoore | |- -. (/) e. Moore_ |
|
| 5 | 4 | a1i | |- ( -. A e. _V -> -. (/) e. Moore_ ) |
| 6 | 3 5 | eqneltrd | |- ( -. A e. _V -> -. { A } e. Moore_ ) |
| 7 | 6 | con4i | |- ( { A } e. Moore_ -> A e. _V ) |
| 8 | 1 7 | impbii | |- ( A e. _V <-> { A } e. Moore_ ) |