These are definitions and proofs involving the "allsome one" quantifier, which extends the "allsome" quantifier of the previous section in the same way that (df-eu) extends .
Some systems extend "there exists" by appending a character to it. If a system provides such an extension, it should provide it for allsome as well: append the same character, let it modify allsome's existence conjunct, and change nothing else. Appending "!" gives "allsome one", so means that is true whenever is true and that exactly one satisfies .
This is what the English word "the" usually does. "The king is hungry" claims that a king exists, that there is only one, and that he is hungry, and the form claims exactly that kind of statement (specifically when means is a king and means is hungry). English says all of that in a single phrase, and the first two have a dedicated word ("the") for the construct. Many other languages have their own dedicated way of saying this. Languages reserve that kind of compression for what their speakers need constantly, which is a good reason for a formal notation to be able to say it just as directly, rather than spelling it out afresh as a conjunction of two quantified formulas every time it comes up. Russell analyzed such definite descriptions with this apparatus in "On Denoting", where his example of a phrase that appears to refer to someone but in fact denotes no one at all is "the present King of France", item (1) of [Russell1905] p. 479, France being a republic that has no king. Write "the king is hungry" as instead and only the last of those three claims survives. The existence claim is silently gone, since that formula is vacuously true when there is no king, and the uniqueness claim is silently gone as well, since that formula holds just the same when there are five kings. Russell reached the opposite verdict for the same example, remarking that every proposition of the form "the present King of France ..." is false, [Russell1905] p. 482. The reason to care is the reason that motivates allsome, only more so; see alimp-surprise and empty-surprise.
Note that this is not merely a way of writing . Reading as "is a king" and as "is hungry", says that there is exactly one hungry king, whereas says that there is exactly one king and that he is hungry. The first is true in a region with five kings exactly one of whom is hungry; the second is false there. Uniqueness attaches to the antecedent, not to the conjunction. See dfalseu2 for the exact relationship between the two and alseueu for the one direction that does hold.
Naming: "alseu" is allsome ("als", as in df-als) extended with "exactly one" ("eu", as in df-eu). The form restricted to a class is prefixed with "r", following df-rals and df-reu, giving df-ralseu.
Soundness: df-alseu and df-ralseu are eliminable and conservative directly, so neither needs a justification theorem. Definitions are required to be eliminable and conservative; see the section comment for df-bi. Each is a biconditional whose left side is a new syntax construct (walseu or wralseu) applied to distinct metavariables, and whose right side uses only constructs introduced earlier (, , , , and the restricted quantifiers df-ral and df-reu), so any occurrence of the new construct can be replaced by the right side, which is eliminability. Conservativity follows, since a proof of a statement not mentioning can have every use of the definition replaced in this way. Every variable occurring on the right side already occurs on the left side, so no dummy variable is introduced, and introducing a dummy variable whose choice must be shown not to matter is the only circumstance here that would call for a justification theorem.
For more, see "The Allsome Quantifier" by David A. Wheeler at https://dwheeler.com/essays/allsome.html