theorem opt0 (A: set): $ 0 e. Option A $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elopt | 0 e. Option A <-> 0 = 0 \/ 0 - 1 e. A |
|
2 | orl | 0 = 0 -> 0 = 0 \/ 0 - 1 e. A |
|
3 | eqid | 0 = 0 |
|
4 | 2, 3 | ax_mp | 0 = 0 \/ 0 - 1 e. A |
5 | 1, 4 | mpbir | 0 e. Option A |