Remove dmxpid from iset.mm
Remove dmxpid from iset.mm

This theorem uses case elimination. The case where A is inhabited
(presumably the interesting one) is just an instance of dmxpm .

metamath/set.mm,metamath/set.mm,metamath/set.mm