Intuitionize abvor0 in iset.mm
Intuitionize abvor0 in iset.mm

Rename to abvor0dc and add the condition that ph is decidable.

Since this is unused in set.mm, there isn't much reason to prefer
this compared with other alternatives like
  -. { x | ph } = _V -> { x | ph } = (/)

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