Merged into my mathbox https://github.com/metamath/set.mm/pull/5380

[David A. Wheeler]

All: I created a PR that affects *only* my mathbox that
makes some changes to my proposed "allsome" quantifier:
https://github.com/metamath/set.mm/pull/5380

I then accidentally merged it while I was distracted by some
other things. My apologies.

It *only* affects my mathbox, so hopefully all is okay.
However, if anyone has any comments, please post on that PR
(or separately), I didn't mean to skip review.

Thanks!

--- David A. Wheeler