Add exmodc to iset.mm
Add exmodc to iset.mm

At least to look at it, exmo sure looks like something that should
only hold given a decidability condition.  Certainly it is
straightforward to show given DECID E. x ph.

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