These are definitions and proofs involving an experimental "allsome" quantifier (aka "all some").
In informal language, statements like "All Martians are green" imply that there is at least one Martian. But it's easy to mistranslate informal language into formal notations because similar statements like do not imply that is ever true, leading to vacuous truths. See alimp-surprise and empty-surprise as examples of the problem. Some systems include a mechanism to counter this, e.g., PVS allows types to be appended with "+" to declare that they are nonempty. This section presents a different solution to the same problem.
The "allsome" quantifier expressly includes the notion of both "all" and "there exists at least one" (aka some), and is defined to make it easier to more directly express both notions. The hope is that if a quantifier more directly expresses this concept, it will be used instead and reduce the risk of creating formal expressions that look okay but in fact are mistranslations. The term "allsome" was chosen because it's short, easy to say, and clearly hints at the two concepts it combines.
I do not expect this to be used much in Metamath, because in Metamath there's a general policy of avoiding the use of new definitions unless there are very strong reasons to do so. Instead, my goal is to rigorously define this quantifier and demonstrate a few basic properties of it.
The syntax allows two forms that look like they would be problematic, but they are fine. When applied to a top-level implication we allow , and when restricted (applied to a class) we allow . The first symbol after the setvar variable must always be if it is the form applied to a class, and since cannot begin a wff, it is unambiguous. The looks like it would be a problem because or might include implications, but any implication arrow within any wff must be surrounded by parentheses, so only the implication arrow of can follow the wff. The implication syntax would work fine without the parentheses, but I added the parentheses because it makes things clearer inside larger complex expressions, and it's also more consistent with the rest of the syntax.
For more, see "The Allsome Quantifier" by David A. Wheeler at https://dwheeler.com/essays/allsome.html I hope that others will eventually agree that allsome is awesome.