theorem lmemconsid (a l: nat): $ a IN a : l $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmemS | a IN a : l <-> a = a \/ a IN l |
|
2 | orl | a = a -> a = a \/ a IN l |
|
3 | eqid | a = a |
|
4 | 2, 3 | ax_mp | a = a \/ a IN l |
5 | 1, 4 | mpbir | a IN a : l |