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