Is there a notation for the unique value that satisfies a predicate

Question

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.

Answer 1

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$".