theorem xp01 (A: set): $ Xp 0 A == 0 $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eq0al | Xp 0 A == 0 <-> A. x ~x e. Xp 0 A |
|
2 | xpfst | x e. Xp 0 A -> fst x e. 0 |
|
3 | el02 | ~fst x e. 0 |
|
4 | 2, 3 | mt | ~x e. Xp 0 A |
5 | 4 | ax_gen | A. x ~x e. Xp 0 A |
6 | 1, 5 | mpbir | Xp 0 A == 0 |