Description: Disjointness of the singletons containing 0 and 1. This is a consequence of bj-disjcsn but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-disjsn01 | |- ( { (/) } i^i { 1o } ) = (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1n0 | |- 1o =/= (/) |
|
| 2 | 1 | necomi | |- (/) =/= 1o |
| 3 | disjsn2 | |- ( (/) =/= 1o -> ( { (/) } i^i { 1o } ) = (/) ) |
|
| 4 | 2 3 | ax-mp | |- ( { (/) } i^i { 1o } ) = (/) |