Description: The only subclass of the empty class is itself. (Contributed by NM, 7-Mar-2007) (Proof shortened by Andrew Salmon, 26-Jun-2011) Strengthen sseq0 to a biconditional. (Revised by BJ, 19-Jul-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sseq0b | |- ( A = (/) -> ( B C_ A <-> B = (/) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sseq2 | |- ( A = (/) -> ( B C_ A <-> B C_ (/) ) ) |
|
| 2 | ss0b | |- ( B C_ (/) <-> B = (/) ) |
|
| 3 | 1 2 | bitrdi | |- ( A = (/) -> ( B C_ A <-> B = (/) ) ) |