theorem all0 (A: set): $ all A 0 $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | absurd | ~x e. lmems 0 -> x e. lmems 0 -> x e. A |
|
2 | lmem0 | ~x IN 0 |
|
3 | 2 | conv lmem | ~x e. lmems 0 |
4 | 1, 3 | ax_mp | x e. lmems 0 -> x e. A |
5 | 4 | ax_gen | A. x (x e. lmems 0 -> x e. A) |
6 | 5 | conv all, subset | all A 0 |