theorem elb10 (b: nat): $ 0 e. b1 b $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elb1 | 0 e. b1 b <-> 0 = 0 \/ 0 - 1 e. b |
|
2 | orl | 0 = 0 -> 0 = 0 \/ 0 - 1 e. b |
|
3 | eqid | 0 = 0 |
|
4 | 2, 3 | ax_mp | 0 = 0 \/ 0 - 1 e. b |
5 | 1, 4 | mpbir | 0 e. b1 b |