Is there a notation for the unique value that satisfies a predicate? Let's say that we have a predicate $\phi$ such that $\exists!x.\phi(x)$. Is there a notation for denoting the unique value of $\phi$? Of course you can just say "let $x$ be the unique value such that $\phi(x)$", but that's a phrase, not a notation. There's a "hacky" ways to accomplish this $$\bigcup_{x \in \\{x | \phi(x)\\}}x \text { (you can also do this with $\bigcap, \sum, \prod, \inf, \sup, \min, \max$, expected value, etc...)}$$ but that obviously is rather confusing. You can do it nicely with Hilbert's epsilon ($\epsilon x. \phi(x)$), but it does not require that $\phi$ has a unique value satisfying it. It doesn't even require $\phi$ to satisfied by _any_ value. I suppose something like $\epsilon !x.\phi(x)$ would work, but I have never seen anybody use that notation before.

> Following the example of _Principia Mathematica_, it is customary [ _sic_ !] to use a definite description operator symbolized using the "turned" (rotated) Greek lower case iota character "$\iota$" [it must be "\turnediota"].

The notation $\iota x (\phi x)$ means

> "$\text { the unique } x \text { such that } \phi x$".