theorem lmem0 (a: nat): $ ~a IN 0 $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elneq2 | lmems 0 = 0 -> (a e. lmems 0 <-> a e. 0) |
|
| 2 | 1 | conv lmem | lmems 0 = 0 -> (a IN 0 <-> a e. 0) |
| 3 | lmems0 | lmems 0 = 0 |
|
| 4 | 2, 3 | ax_mp | a IN 0 <-> a e. 0 |
| 5 | el02 | ~a e. 0 |
|
| 6 | 4, 5 | mtbir | ~a IN 0 |