Intuitionize uni0b in iset.mm
Intuitionize uni0b in iset.mm

The statement of the theorem is unchanged. The proof is also fairly
similar, relying on elsn , dfss3 , rexcom4 , and eluni2 . However,
it needs a fair bit of rearrangement to be based on eq0 rather than
neq0 .

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