Add dtruex and dtru to iset.mm
Add dtruex and dtru to iset.mm

The dtru proof here is very different from the set.mm one (because
we actually construct a set distinct from y), but we can prove the
theorem as stated in set.mm.

We also want a theorem, dtruex , stated in terms of E. rather than
A. . Without the law of the excluded middle, dtruex implies dtru
but not the converse.

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