More decidability in iset.mm.
More decidability in iset.mm.

Add pm2.61ddc, counterpart to pm2.61d for a decidable proposition.

Replace bija with bijadc to remove ax-3 usage.

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